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

Class BasicLoopExecutionSnippet

java.lang.Object

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

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

All Implemented Interfaces:

FactoryMethod

public class BasicLoopExecutionSnippet
extends ReplaceAndRegisterMethod
implements FactoryMethod

Constructor Summary

Constructors

Constructor and Description
BasicLoopExecutionSnippet()

Method Summary

Modifier and Type	Method and Description
private Pair<JavaBlock,JavaBlock>	buildJavaBlock(BasicSnippetData d)
private Term	buildProgramTerm(BasicSnippetData d, ProofObligationVars vs, Term postTerm, TermBuilder tb)
Term	produce(BasicSnippetData d, ProofObligationVars poVars)

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

collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables

Methods inherited from class java.lang.Object

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

Constructor Detail

BasicLoopExecutionSnippet

public BasicLoopExecutionSnippet()

Method Detail

produce

public Term produce(BasicSnippetData d,
                    ProofObligationVars poVars)
             throws java.lang.UnsupportedOperationException

Specified by:

produce in interface FactoryMethod

Throws:

java.lang.UnsupportedOperationException

buildProgramTerm

private Term buildProgramTerm(BasicSnippetData d,
                              ProofObligationVars vs,
                              Term postTerm,
                              TermBuilder tb)

buildJavaBlock

private Pair<JavaBlock,JavaBlock> buildJavaBlock(BasicSnippetData d)