public class ContractFactory
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
INFORMATION_FLOW_CONTRACT_BASENAME
The base name for information flow contracts.
|
static java.lang.String |
SYMB_EXEC_CONTRACT_BASENAME
The base name for symbolic execution contracts.
|
Constructor and Description |
---|
ContractFactory(Services services)
Creates a new contract factory.
|
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
addGlobalDefs(FunctionalOperationContract opc,
Term globalDefs)
Add global variable definitions (aka.
|
FunctionalOperationContract |
addPost(FunctionalOperationContract old,
InitiallyClause ini)
Add the specification contained in InitiallyClause as a postcondition.
|
FunctionalOperationContract |
addPost(FunctionalOperationContract old,
Term addedPost,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
postcondition (regardless of termination case).
|
FunctionalOperationContract |
addPre(FunctionalOperationContract old,
Term addedPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars)
Returns another contract like this one, except that the passed term has been added as a
precondition.
|
InformationFlowContract |
createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
DependencyContract |
dep(KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
DependencyContract |
dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
DependencyContract |
dep(java.lang.String string,
KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
boolean |
equals(java.lang.Object o) |
FunctionalOperationContract |
func(IProgramMethod pm,
InitiallyClause ini)
|
FunctionalOperationContract |
func(java.lang.String baseName,
IProgramMethod pm,
boolean terminates,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariableCollection pv)
Creates a new functional operation contract.
|
FunctionalOperationContract |
func(java.lang.String baseName,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accessibles,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariableCollection progVars,
boolean toBeSaved,
boolean transaction)
Creates a new functional operation contract.
|
FunctionalOperationContract |
func(java.lang.String baseName,
KeYJavaType kjt,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accs,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
boolean toBeSaved)
Creates a new functional operation contract.
|
FunctionalBlockContract |
funcBlock(BlockContract blockContract)
Create a new
FunctionalBlockContract from an existing BlockContract . |
FunctionalLoopContract |
funcLoop(LoopContract loopContract)
Create a new
FunctionalLoopContract from an existing LoopContract . |
static java.lang.String |
generateContractName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
static java.lang.String |
generateContractTypeName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn) |
static java.lang.String |
generateDisplayName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
int |
hashCode() |
FunctionalOperationContract |
union(FunctionalOperationContract... contracts)
Returns the union of the passed contracts.
|
public static final java.lang.String SYMB_EXEC_CONTRACT_BASENAME
public static final java.lang.String INFORMATION_FLOW_CONTRACT_BASENAME
public ContractFactory(Services services)
services
- the services objectpublic FunctionalOperationContract addPost(FunctionalOperationContract old, Term addedPost, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars)
old
- the old contractaddedPost
- the post condition to be addedselfVar
- the used self variableresultVar
- the used result variableexcVar
- the used exception variableparamVars
- the used program variablesatPreVars
- the used pre-heap variablespublic FunctionalOperationContract addPost(FunctionalOperationContract old, InitiallyClause ini)
old
- the old contractini
- the initially clause to be addedpublic FunctionalOperationContract addPre(FunctionalOperationContract old, Term addedPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars)
old
- the old contractaddedPre
- precondition to be addedselfVar
- used self variableparamVars
- used program variablesatPreVars
- used pre-heap variablespublic FunctionalOperationContract addGlobalDefs(FunctionalOperationContract opc, Term globalDefs)
opc
- the functional method contractglobalDefs
- the global variable definitionspublic DependencyContract dep(KeYJavaType containerType, IObserverFunction pm, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> requires, Term measuredBy, java.util.Map<ProgramVariable,Term> accessibles, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Term globalDefs)
public DependencyContract dep(KeYJavaType kjt, LocationVariable targetHeap, Triple<IObserverFunction,Term,Term> dep, ProgramVariable selfVar)
public DependencyContract dep(java.lang.String string, KeYJavaType containerType, IObserverFunction pm, KeYJavaType specifiedIn, java.util.Map<LocationVariable,Term> requires, Term measuredBy, java.util.Map<ProgramVariable,Term> accessibles, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars, Term globalDefs)
public InformationFlowContract createInformationFlowContract(KeYJavaType forClass, IProgramMethod pm, KeYJavaType specifiedIn, Modality modality, Term requires, Term requiresFree, Term measuredBy, Term modifies, boolean hasMod, ProgramVariableCollection progVars, Term accessible, ImmutableList<InfFlowSpec> infFlowSpecs, boolean toBeSaved)
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public FunctionalBlockContract funcBlock(BlockContract blockContract)
FunctionalBlockContract
from an existing BlockContract
.blockContract
- the BlockContract
.FunctionalBlockContract
.public FunctionalLoopContract funcLoop(LoopContract loopContract)
FunctionalLoopContract
from an existing LoopContract
.loopContract
- the LoopContract
.FunctionalLoopContract
.public FunctionalOperationContract func(IProgramMethod pm, InitiallyClause ini) throws SLTranslationException
pm
- the IProgramMethod
.ini
- the InitiallyClause
.FunctionalOperationContract
.SLTranslationException
- in case translating the initially clause fails.public FunctionalOperationContract func(java.lang.String baseName, KeYJavaType kjt, IProgramMethod pm, Modality modality, java.util.Map<LocationVariable,Term> pres, java.util.Map<LocationVariable,Term> freePres, Term mby, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> freePosts, java.util.Map<LocationVariable,Term> axioms, java.util.Map<LocationVariable,Term> mods, java.util.Map<ProgramVariable,Term> accs, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,LocationVariable> atPreVars, boolean toBeSaved)
baseName
- base name of the contract (does not have to be unique)kjt
- the KeYJavaType of the classpm
- the IProgramMethod to which the contract belongsmodality
- the modality of the contractpres
- the precondition of the contractfreePres
- the free/unchecked precondition of the contractmby
- the measured_by clause of the contractposts
- the postcondition of the contractfreePosts
- the free/unchecked postcondition of the contractaxioms
- the class axioms of the methodmods
- the modifies clause of the contractaccs
- the dependency clause of the contracthasMod
- whether the contract has a modifies setselfVar
- the self variableparamVars
- the parameter variablesresultVar
- the exception variableexcVar
- the result variableatPreVars
- a map of all pre-heap variablestoBeSaved
- TODOpublic FunctionalOperationContract func(java.lang.String baseName, IProgramMethod pm, boolean terminates, java.util.Map<LocationVariable,Term> pres, java.util.Map<LocationVariable,Term> freePres, Term mby, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> freePosts, java.util.Map<LocationVariable,Term> axioms, java.util.Map<LocationVariable,Term> mods, java.util.Map<ProgramVariable,Term> accessibles, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, ProgramVariableCollection pv)
baseName
- base name of the contract (does not have to be unique)pm
- the IProgramMethod to which the contract belongsterminates
- a boolean determining whether we also prove terminationpres
- the precondition of the contractfreePres
- the free/unchecked precondition of the contractmby
- the measured_by clause of the contractposts
- the postcondition of the contractfreePosts
- the free/unchecked postcondition of the contractaxioms
- the class axioms of the methodmods
- the modifies clause of the contractaccessibles
- the dependency clause of the contracthasMod
- whether the contract has a modifies setpv
- a collection of the program variablespublic FunctionalOperationContract func(java.lang.String baseName, IProgramMethod pm, Modality modality, java.util.Map<LocationVariable,Term> pres, java.util.Map<LocationVariable,Term> freePres, Term mby, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> freePosts, java.util.Map<LocationVariable,Term> axioms, java.util.Map<LocationVariable,Term> mods, java.util.Map<ProgramVariable,Term> accessibles, java.util.Map<LocationVariable,java.lang.Boolean> hasMod, ProgramVariableCollection progVars, boolean toBeSaved, boolean transaction)
baseName
- base name of the contract (does not have to be unique)pm
- the IProgramMethod to which the contract belongsmodality
- the modality of the contractpres
- the precondition of the contractfreePres
- the free/unchecked precondition of the contractmby
- the measured_by clause of the contractposts
- the postcondition of the contractfreePosts
- the free/unchecked postcondition of the contractaxioms
- the class axioms of the methodmods
- the modifies clause of the contractaccessibles
- the dependency clause of the contracthasMod
- whether the contract has a modifies setprogVars
- the program variablestoBeSaved
- TODOtransaction
- TODOpublic FunctionalOperationContract union(FunctionalOperationContract... contracts)
contracts
- the passed contractspublic int hashCode()
hashCode
in class java.lang.Object
public static java.lang.String generateDisplayName(java.lang.String baseName, KeYJavaType forClass, IObserverFunction target, KeYJavaType specifiedIn, int myId)
public static java.lang.String generateContractName(java.lang.String baseName, KeYJavaType forClass, IObserverFunction target, KeYJavaType specifiedIn, int myId)
public static java.lang.String generateContractTypeName(java.lang.String baseName, KeYJavaType forClass, IObserverFunction target, KeYJavaType specifiedIn)
Copyright © 2003-2019 The KeY-Project.