abstract class TwoStateMethodPredicateSnippet extends java.lang.Object implements FactoryMethod
Constructor and Description |
---|
TwoStateMethodPredicateSnippet() |
Modifier and Type | Method and Description |
---|---|
private ImmutableList<Term> |
extractTermListForPredicate(IProgramMethod pm,
ProofObligationVars poVars,
boolean hasMby)
Parameters and the result of a method only have to appear once in the
predicate.
|
protected Sort[] |
generateContApplArgumentSorts(ImmutableList<Term> termList,
IProgramMethod pm) |
private Function |
generateContApplPredicate(java.lang.String nameString,
Sort[] argSorts,
TermBuilder tb,
Services services) |
(package private) abstract java.lang.String |
generatePredicateName(IProgramMethod pm,
StatementBlock block,
LoopSpecification loopInv) |
private Term |
instantiateContApplPredicate(Function pred,
ImmutableList<Term> termList,
TermBuilder tb) |
Term |
produce(BasicSnippetData d,
ProofObligationVars poVars) |
public Term produce(BasicSnippetData d, ProofObligationVars poVars) throws java.lang.UnsupportedOperationException
produce
in interface FactoryMethod
java.lang.UnsupportedOperationException
protected Sort[] generateContApplArgumentSorts(ImmutableList<Term> termList, IProgramMethod pm)
private Function generateContApplPredicate(java.lang.String nameString, Sort[] argSorts, TermBuilder tb, Services services)
private Term instantiateContApplPredicate(Function pred, ImmutableList<Term> termList, TermBuilder tb)
abstract java.lang.String generatePredicateName(IProgramMethod pm, StatementBlock block, LoopSpecification loopInv)
private ImmutableList<Term> extractTermListForPredicate(IProgramMethod pm, ProofObligationVars poVars, boolean hasMby)
poVars
- The proof obligation variables.