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

Class SelfcomposedLoopSnippet

java.lang.Object

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

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

All Implemented Interfaces:

InfFlowFactoryMethod

public class SelfcomposedLoopSnippet
extends ReplaceAndRegisterMethod
implements InfFlowFactoryMethod

Constructor Summary

Constructors

Constructor and Description
SelfcomposedLoopSnippet()

Method Summary

Modifier and Type	Method and Description
Term	produce(BasicSnippetData d, ProofObligationVars poVars1, ProofObligationVars poVars2)

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

SelfcomposedLoopSnippet

public SelfcomposedLoopSnippet()

Method Detail

produce

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

Specified by:

produce in interface InfFlowFactoryMethod

Throws:

java.lang.UnsupportedOperationException