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

Class POSnippetFactory

java.lang.Object

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

public class POSnippetFactory
extends java.lang.Object

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
POSnippetFactory()

Method Summary

Modifier and Type	Method and Description
(package private) static BasicPOSnippetFactory	getBasicFactory(BasicSnippetData data, ProofObligationVars poVars)
static BasicPOSnippetFactory	getBasicFactory(BlockContract contract, ProofObligationVars vars, ExecutionContext context, Services services)
static BasicPOSnippetFactory	getBasicFactory(FunctionalOperationContract contract, ProofObligationVars vars, Services services)
static BasicPOSnippetFactory	getBasicFactory(InformationFlowContract contract, ProofObligationVars vars, Services services)
static BasicPOSnippetFactory	getBasicFactory(LoopSpecification invariant, ProofObligationVars vars, ExecutionContext context, Term guardTerm, Services services)
(package private) static InfFlowPOSnippetFactory	getInfFlowFactory(BasicSnippetData data, ProofObligationVars vars1, ProofObligationVars vars2)
static InfFlowPOSnippetFactory	getInfFlowFactory(BlockContract contract, ProofObligationVars vars1, ProofObligationVars vars2, ExecutionContext context, Services services)
static InfFlowPOSnippetFactory	getInfFlowFactory(InformationFlowContract contract, ProofObligationVars vars1, ProofObligationVars vars2, Services services)
static InfFlowPOSnippetFactory	getInfFlowFactory(LoopSpecification invariant, ProofObligationVars vars1, ProofObligationVars vars2, ExecutionContext context, Term guardTerm, Services services)

Methods inherited from class java.lang.Object

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

Constructor Detail

POSnippetFactory

public POSnippetFactory()

Method Detail

getBasicFactory

public static BasicPOSnippetFactory getBasicFactory(FunctionalOperationContract contract,
                                                    ProofObligationVars vars,
                                                    Services services)

getBasicFactory

public static BasicPOSnippetFactory getBasicFactory(LoopSpecification invariant,
                                                    ProofObligationVars vars,
                                                    ExecutionContext context,
                                                    Term guardTerm,
                                                    Services services)

getBasicFactory

public static BasicPOSnippetFactory getBasicFactory(InformationFlowContract contract,
                                                    ProofObligationVars vars,
                                                    Services services)

getBasicFactory

public static BasicPOSnippetFactory getBasicFactory(BlockContract contract,
                                                    ProofObligationVars vars,
                                                    ExecutionContext context,
                                                    Services services)

getBasicFactory

static BasicPOSnippetFactory getBasicFactory(BasicSnippetData data,
                                             ProofObligationVars poVars)

getInfFlowFactory

public static InfFlowPOSnippetFactory getInfFlowFactory(LoopSpecification invariant,
                                                        ProofObligationVars vars1,
                                                        ProofObligationVars vars2,
                                                        ExecutionContext context,
                                                        Term guardTerm,
                                                        Services services)

getInfFlowFactory

public static InfFlowPOSnippetFactory getInfFlowFactory(InformationFlowContract contract,
                                                        ProofObligationVars vars1,
                                                        ProofObligationVars vars2,
                                                        Services services)

getInfFlowFactory

public static InfFlowPOSnippetFactory getInfFlowFactory(BlockContract contract,
                                                        ProofObligationVars vars1,
                                                        ProofObligationVars vars2,
                                                        ExecutionContext context,
                                                        Services services)

getInfFlowFactory

static InfFlowPOSnippetFactory getInfFlowFactory(BasicSnippetData data,
                                                 ProofObligationVars vars1,
                                                 ProofObligationVars vars2)