Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
protected void |
SymbolicLayoutExtractor.applyCut(ProofStarter starter,
Term term,
int maxProofSteps)
Applies one single cut rule for the given
Term . |
protected void |
SymbolicLayoutExtractor.applyCutRules(ProofStarter starter,
java.util.Set<Term> symbolicObjects,
ImmutableList<Term> updates)
Applies cut rules to the given side proofs to compute equivalence classes.
|
Modifier and Type | Method and Description |
---|---|
static ProofStarter |
SymbolicExecutionSideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
Modifier and Type | Method and Description |
---|---|
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofStarter starter,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof.
|
Modifier and Type | Method and Description |
---|---|
static ProofStarter |
SideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
Copyright © 2003-2019 The KeY-Project.