public class ContractFactory
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
CONTRACT_COMBINATION_MARKER |
static java.lang.String |
INFORMATION_FLOW_CONTRACT_BASENAME |
private static java.lang.String |
INVALID_ID |
private Services |
services |
static java.lang.String |
SYMB_EXEC_CONTRACT_BASENAME |
private TermBuilder |
tb |
private static java.lang.String |
UNKNOWN_CONTRACT_IMPLEMENTATION |
Constructor and Description |
---|
ContractFactory(Services services) |
Modifier and Type | Method and Description |
---|---|
FunctionalOperationContract |
addGlobalDefs(FunctionalOperationContract opc,
Term globalDefs)
Add global variable definitions (aka. old clause) to the contract.
|
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.
|
private static <T> void |
addToMap(T var,
T originalVar,
java.util.Map<T,T> map) |
private Term |
atPreify(Term t,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars) |
private static java.lang.String |
concadinate(java.lang.String delim,
ImmutableArray<KeYJavaType> elems) |
InformationFlowContract |
createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
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) |
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) |
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) |
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() |
private Term |
replaceVariables(Term original,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
ProgramVariable originalSelfVar,
ImmutableList<ProgramVariable> originalParamVars,
java.util.Map<LocationVariable,LocationVariable> originalAtPreVars)
replace in original the variables used for self and parameters
|
private Term |
replaceVariables(Term original,
ProgramVariable selfVar,
ProgramVariable resultVar,
ProgramVariable excVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
ProgramVariable originalExcVar,
ImmutableList<ProgramVariable> originalParamVars,
java.util.Map<LocationVariable,LocationVariable> originalAtPreVars)
replace in original the variables used for self, result, exception, heap, and parameters
|
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
private static final java.lang.String INVALID_ID
private static final java.lang.String UNKNOWN_CONTRACT_IMPLEMENTATION
private static final java.lang.String CONTRACT_COMBINATION_MARKER
private final Services services
private final TermBuilder tb
public ContractFactory(Services services)
public FunctionalOperationContract addPost(FunctionalOperationContract old, Term addedPost, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars)
public FunctionalOperationContract addPost(FunctionalOperationContract old, InitiallyClause ini)
public FunctionalOperationContract addPre(FunctionalOperationContract old, Term addedPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars)
public FunctionalOperationContract addGlobalDefs(FunctionalOperationContract opc, Term globalDefs)
public 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 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
SLTranslationException
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)
public 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)
public 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)
public FunctionalOperationContract union(FunctionalOperationContract... contracts)
private static <T> void addToMap(T var, T originalVar, java.util.Map<T,T> map)
private Term atPreify(Term t, java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars)
private Term replaceVariables(Term original, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, ProgramVariable originalSelfVar, ImmutableList<ProgramVariable> originalParamVars, java.util.Map<LocationVariable,LocationVariable> originalAtPreVars)
private Term replaceVariables(Term original, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,LocationVariable> atPreVars, ProgramVariable originalSelfVar, ProgramVariable originalResultVar, ProgramVariable originalExcVar, ImmutableList<ProgramVariable> originalParamVars, java.util.Map<LocationVariable,LocationVariable> originalAtPreVars)
public 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)
private static java.lang.String concadinate(java.lang.String delim, ImmutableArray<KeYJavaType> elems)