Package | Description |
---|---|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
Modifier and Type | Method and Description |
---|---|
protected static AbstractLoopInvariantRule.AdditionalHeapTerms |
AbstractLoopInvariantRule.createAdditionalHeapTerms(Services services,
AbstractLoopInvariantRule.Instantiation inst,
java.util.List<LocationVariable> heapContext,
ImmutableSet<ProgramVariable> localOuts,
java.util.Map<LocationVariable,java.util.Map<Term,Term>> heapToBeforeLoop,
java.util.Map<LocationVariable,Term> atPres)
Prepare anon update, wellformed formula, frame condition and reachable
state formula.
|
Copyright © 2003-2019 The KeY-Project.