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
Proof s
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) . |