Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Field and Description |
---|---|
protected AuxiliaryContract.Terms |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.terms |
Modifier and Type | Method and Description |
---|---|
AuxiliaryContract.Terms |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.getTerms() |
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpLoopValidityGoal(Goal goal,
LoopContract contract,
Term context,
Term remember,
Term rememberNext,
java.util.Map<LocationVariable,Function> anonOutHeaps,
java.util.Map<LocationVariable,Term> modifiesClauses,
Term[] assumptions,
Term decreasesCheck,
Term[] postconditions,
Term[] postconditionsNext,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms,
AuxiliaryContract.Variables nextVars) |
Term |
AuxiliaryContractBuilders.GoalsConfigurator.setUpValidityGoal(Goal goal,
Term[] updates,
Term[] assumptions,
Term[] postconditions,
ProgramVariable exceptionParameter,
AuxiliaryContract.Terms terms) |
Modifier and Type | Method and Description |
---|---|
AuxiliaryContract.Terms |
AbstractAuxiliaryContractImpl.getVariablesAsTerms(Services services) |
AuxiliaryContract.Terms |
AuxiliaryContract.getVariablesAsTerms(Services services) |
AuxiliaryContract.Terms |
AuxiliaryContract.Variables.termify(Term self) |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Term,Term> |
AbstractAuxiliaryContractImpl.createReplacementMap(Term newHeap,
AuxiliaryContract.Terms newTerms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getFreePrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
java.lang.String |
AbstractAuxiliaryContractImpl.getPlainText(Services services,
AuxiliaryContract.Terms terms) |
java.lang.String |
AuxiliaryContract.getPlainText(Services services,
AuxiliaryContract.Terms terms) |
Term |
AbstractAuxiliaryContractImpl.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPostcondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AuxiliaryContract.getPrecondition(LocationVariable heapVariable,
Term heap,
AuxiliaryContract.Terms terms,
Services services) |
Term |
AbstractAuxiliaryContractImpl.getTerm(Term term,
Term heap,
AuxiliaryContract.Terms terms,
Services services)
Replaces variables in a map of terms
|
Copyright © 2003-2019 The KeY-Project.