All Methods Static Methods Instance Methods Concrete Methods
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,
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,
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,
Map<T,T> map) |
private Term |
atPreify(Term t,
Map<LocationVariable,? extends ProgramVariable> atPreVars) |
private static String |
concadinate(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,
Map<LocationVariable,Term> requires,
Term measuredBy,
Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
DependencyContract |
dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
DependencyContract |
dep(String string,
KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
Map<LocationVariable,Term> requires,
Term measuredBy,
Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
boolean |
equals(Object o) |
FunctionalOperationContract |
func(IProgramMethod pm,
InitiallyClause ini) |
FunctionalOperationContract |
func(String baseName,
IProgramMethod pm,
boolean terminates,
Map<LocationVariable,Term> pres,
Map<LocationVariable,Term> freePres,
Term mby,
Map<LocationVariable,Term> posts,
Map<LocationVariable,Term> freePosts,
Map<LocationVariable,Term> axioms,
Map<LocationVariable,Term> mods,
Map<ProgramVariable,Term> accessibles,
Map<LocationVariable,Boolean> hasMod,
ProgramVariableCollection pv) |
FunctionalOperationContract |
func(String baseName,
IProgramMethod pm,
Modality modality,
Map<LocationVariable,Term> pres,
Map<LocationVariable,Term> freePres,
Term mby,
Map<LocationVariable,Term> posts,
Map<LocationVariable,Term> freePosts,
Map<LocationVariable,Term> axioms,
Map<LocationVariable,Term> mods,
Map<ProgramVariable,Term> accessibles,
Map<LocationVariable,Boolean> hasMod,
ProgramVariableCollection progVars,
boolean toBeSaved,
boolean transaction) |
FunctionalOperationContract |
func(String baseName,
KeYJavaType kjt,
IProgramMethod pm,
Modality modality,
Map<LocationVariable,Term> pres,
Map<LocationVariable,Term> freePres,
Term mby,
Map<LocationVariable,Term> posts,
Map<LocationVariable,Term> freePosts,
Map<LocationVariable,Term> axioms,
Map<LocationVariable,Term> mods,
Map<ProgramVariable,Term> accs,
Map<LocationVariable,Boolean> hasMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
Map<LocationVariable,LocationVariable> atPreVars,
boolean toBeSaved) |
static String |
generateContractName(String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
static String |
generateContractTypeName(String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn) |
static String |
generateDisplayName(String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
int |
hashCode() |
private Term |
replaceVariables(Term original,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Map<LocationVariable,LocationVariable> atPreVars,
ProgramVariable originalSelfVar,
ImmutableList<ProgramVariable> originalParamVars,
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,
Map<LocationVariable,LocationVariable> atPreVars,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
ProgramVariable originalExcVar,
ImmutableList<ProgramVariable> originalParamVars,
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.
|