| Class | Description |
|---|---|
| DefaultEntry<K,V> | |
| EqualsHashCodeResetter<T> |
Instances of this class are used to reset overwritten
Object.equals(Object)
and Object.hashCode() methods of the wrapped child element to the
default Java implementation with referenced based equality. |
| SideProofStore |
The only instance of this class
SideProofStore.DEFAULT_INSTANCE is used
to manage performed side proofs. |
| SideProofStore.Entry |
An
SideProofStore.Entry of a SideProofStore. |
| SymbolicExecutionEnvironment<U extends UserInterfaceControl> |
Instances of this class are used to collect and access all
relevant information for symbolic execution tree extraction of
Proofs
via an SymbolicExecutionTreeBuilder. |
| SymbolicExecutionSideProofUtil |
Provides utility methods for side proofs.
|
| SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor |
Utility class used by
QuerySideProofRule#containsIrrelevantThings(Services, SequentFormula, Set). |
| SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor |
Utility method used by
QuerySideProofRule#containsModalityOrQuery(Term). |
| SymbolicExecutionUtil |
Provides utility methods for symbolic execution with KeY.
|
| SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult | |
| SymbolicExecutionUtil.FindModalityWithSymbolicExecutionLabelId |
Utility class used to find the maximal modality Term
used by
SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Term). |
| SymbolicExecutionUtil.SiteProofVariableValueInput |
Helper class which represents the return value of
ExecutionMethodReturn#createExtractReturnVariableValueSequent(TypeReference, ReferencePrefix, Node, IProgramVariable) and
ExecutionMethodReturn#createExtractVariableValueSequent(IExecutionContext, Node, IProgramVariable). |