abstract class TwoStateMethodPredicateSnippet extends 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(String nameString,
Sort[] argSorts,
TermBuilder tb,
Services services) |
(package private) abstract String |
generatePredicateName(IProgramMethod pm,
StatementBlock block,
LoopInvariant 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 UnsupportedOperationException
produce
in interface FactoryMethod
UnsupportedOperationException
protected Sort[] generateContApplArgumentSorts(ImmutableList<Term> termList, IProgramMethod pm)
private Function generateContApplPredicate(String nameString, Sort[] argSorts, TermBuilder tb, Services services)
private Term instantiateContApplPredicate(Function pred, ImmutableList<Term> termList, TermBuilder tb)
abstract String generatePredicateName(IProgramMethod pm, StatementBlock block, LoopInvariant loopInv)
private ImmutableList<Term> extractTermListForPredicate(IProgramMethod pm, ProofObligationVars poVars, boolean hasMby)
poVars
- The proof obligation variables.