DependencyContract |
ContractFactory.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 |
ContractFactory.dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
DependencyContract |
ContractFactory.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) |
DependencyContract |
DependencyContractImpl.map(java.util.function.UnaryOperator<Term> op,
Services services) |
DependencyContract |
DependencyContract.map(java.util.function.UnaryOperator<Term> op,
Services services) |
DependencyContract |
DependencyContractImpl.setID(int newId) |