Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.util.mergerule |
Class and Description |
---|
SymbolicExecutionState
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
Class and Description |
---|
SymbolicExecutionState
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
SymbolicExecutionStateWithProgCnt
A symbolic execution state with program counter is a triple of a symbolic
state in form of a parallel update, a path condition in form of a JavaDL
formula, and a program counter in form of a JavaDL formula with non-empty
Java Block (and a possible post condition as first, and only, sub term).
|
Class and Description |
---|
SymbolicExecutionState
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
Class and Description |
---|
MergeParamsSpec
Specification of merge parameters for the creation of
MergeContract s; |
Class and Description |
---|
MergeRuleUtils.Option
A simple Scala-like option type: Either Some(value) or None.
|
SymbolicExecutionState
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
SymbolicExecutionStateWithProgCnt
A symbolic execution state with program counter is a triple of a symbolic
state in form of a parallel update, a path condition in form of a JavaDL
formula, and a program counter in form of a JavaDL formula with non-empty
Java Block (and a possible post condition as first, and only, sub term).
|
Copyright © 2003-2019 The KeY-Project.