de.uka.ilkd.key.informationflow.po.snippet

Class LoopCallWithInvariantPredicateSnippet

java.lang.Object

de.uka.ilkd.key.informationflow.po.snippet.TwoStateMethodPredicateSnippet

de.uka.ilkd.key.informationflow.po.snippet.LoopCallWithInvariantPredicateSnippet

All Implemented Interfaces:

FactoryMethod

public class LoopCallWithInvariantPredicateSnippet
extends TwoStateMethodPredicateSnippet

Constructor Summary

Constructors

Constructor and Description
LoopCallWithInvariantPredicateSnippet()

Method Summary

Modifier and Type	Method and Description
(package private) java.lang.String	generatePredicateName(IProgramMethod pm, StatementBlock block, LoopSpecification loopInv)

Methods inherited from class de.uka.ilkd.key.informationflow.po.snippet.TwoStateMethodPredicateSnippet

generateContApplArgumentSorts, produce

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

LoopCallWithInvariantPredicateSnippet

public LoopCallWithInvariantPredicateSnippet()

Method Detail

generatePredicateName

java.lang.String generatePredicateName(IProgramMethod pm,
                                       StatementBlock block,
                                       LoopSpecification loopInv)

Specified by:

generatePredicateName in class TwoStateMethodPredicateSnippet