| |
|
| java.lang.Object de.uka.ilkd.key.cspec.ComputeSpecification
POSTSTATE_REMEMBER_EQUATIONS | final public static int POSTSTATE_REMEMBER_EQUATIONS(Code) | | Use explicit poststate remember equations
(x1=x1@post & ...& xn=xn@post).
Requires knowledge of the modifies list.
|
POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION | final public static int POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION(Code) | | Use state change accumulatorr ^true alias scripted C for remembering
the poststate.
Does not require knowledge of the modifies list.
false for explicit poststate remember terms
(x1=x1@post & ...& xn=xn@post) which requires knowledge of the modifies list.
|
PRESTATE_REMEMBER_EQUATIONS | final public static int PRESTATE_REMEMBER_EQUATIONS(Code) | | Use explicit prestate remembrance equations.
Thus use proof obligations like x=xpre ← <program> (xpost=x).
|
PRESTATE_REMEMBER_IMPLICIT | final public static int PRESTATE_REMEMBER_IMPLICIT(Code) | | Only remember prestate, implicitly.
Thus use proof obligations like <program> (xpost=x).
|
PRESTATE_REMEMBER_UPDATES | final public static int PRESTATE_REMEMBER_UPDATES(Code) | | Use updates for prestate remembrance.
Thus use proof obligations like {x:=xpre} <program> (xpost=x).
|
ComputeSpecification | public ComputeSpecification()(Code) | | |
getPoststateRemember | final public static int getPoststateRemember()(Code) | | |
getPrestateRemember | final public static int getPrestateRemember()(Code) | | |
|
|
|