class BasicPOSnippetFactoryImpl extends java.lang.Object implements BasicPOSnippetFactory
BasicPOSnippetFactory.Snippet
Modifier and Type | Field and Description |
---|---|
private BasicSnippetData |
data
Collection of data important for the production of snippets.
|
private java.util.EnumMap<BasicPOSnippetFactory.Snippet,FactoryMethod> |
factoryMethods
Registered snippet factory methods.
|
private ProofObligationVars |
poVars
Variables belonging to the proof obligation.
|
Constructor and Description |
---|
BasicPOSnippetFactoryImpl(BasicSnippetData data,
ProofObligationVars poVars) |
BasicPOSnippetFactoryImpl(BlockContract contract,
ProofObligationVars poVars,
ExecutionContext context,
Services services) |
BasicPOSnippetFactoryImpl(FunctionalOperationContract contract,
ProofObligationVars poVars,
Services services) |
BasicPOSnippetFactoryImpl(InformationFlowContract contract,
ProofObligationVars poVars,
Services services) |
BasicPOSnippetFactoryImpl(LoopSpecification invariant,
ProofObligationVars poVars,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
create(BasicPOSnippetFactory.Snippet snippet) |
private void |
registerFactoryMethods() |
private final BasicSnippetData data
private final ProofObligationVars poVars
private final java.util.EnumMap<BasicPOSnippetFactory.Snippet,FactoryMethod> factoryMethods
BasicPOSnippetFactoryImpl(BasicSnippetData data, ProofObligationVars poVars)
BasicPOSnippetFactoryImpl(FunctionalOperationContract contract, ProofObligationVars poVars, Services services)
BasicPOSnippetFactoryImpl(LoopSpecification invariant, ProofObligationVars poVars, ExecutionContext context, Term guardTerm, Services services)
BasicPOSnippetFactoryImpl(InformationFlowContract contract, ProofObligationVars poVars, Services services)
BasicPOSnippetFactoryImpl(BlockContract contract, ProofObligationVars poVars, ExecutionContext context, Services services)
private void registerFactoryMethods()
public Term create(BasicPOSnippetFactory.Snippet snippet) throws java.lang.UnsupportedOperationException
create
in interface BasicPOSnippetFactory
java.lang.UnsupportedOperationException