As of March 15, 2011, this page is no longer maintained. KeYHeap has become the regular development version of KeY (version 1.7), and is scheduled to replace the stable release version KeY 1.6 in the future. For up-to-date information see the KeY download page.
"KeYHeap" is the working title of a major revision of the KeY system
that is currently under development. At its core, KeYHeap is a deductive verifier for
sequential Java programs wrt. specifications written in a crossover between
JML and dynamic
frames. Unlike all KeY versions <= 1.6, KeYHeap uses a heap model like that of typical
verifiers (in particular VeriCool and
which also use dynamic frames style specifications).
Download the Latest KeY Development Version
[Internal wiki page]
- New heap model
- Sorts "Heap" and "Field", functions "select", "store", "create", "anon", program variable "heap"
- "o.f" means "select(heap, o, f)" instead of "f(o)"
- Functions with heap as argument instead of location dependent functions
- Set-typed terms instead of location descriptors
- More straightforward encoding of the correctness of modifies clauses, using quantification over locations
- Reasoning about location sets (empty sets, singleton sets, union, intersection, set difference, set comprehension)
- Simplified model of object allocation
- Allocation "new MyClass()" takes an unspecified object satisfying "o.<created>=FALSE & MyClass::exactInstance(o)=TRUE"
- No need for allocation counters "MyClass.<nextToCreate>" and object enumerators "MyClass::<get>"
- Constant domain assumption still in effect
- Adapted JML frontend and proof management
- Type \locset in specifications (dynamic frames)
- Model fields and dependencies
- Modifies clauses implictly allow object allocation and initialisation
- Invariants as model field \inv instead of visible state semantics or observed state semantics
- Method contract rule discharges whole method call including dynamic dispatch (behavioural subtyping)
- Type \seq in specifications (finite mathematical sequences)
- Rule-based update simplification
- Ca. 20 rewrite taclets (using two special, but simple "variable conditions") instead of one large built-in rule
- Optional "one-step simplification": Meta-rule that eagerly applies rewrite rules in the "concrete" and "simplify" categories as a single proof step
- One-step simplification plays similar role as update simplifier in normal KeY, but is not limited to updates
- Simplified representation of integers
- One sort "int" instead of the hierarchy of "int", "jbyte", "jchar", "jint", "jlong", "jshort", "integerDomain"
- Different choices for handling overflows (ignore, check, be Java-faithful) still supported
- ArrayStoreException still handled correctly
- Code refactoring
- Cleaned up implementation of core data structures (sorts, operators, terms, formulas, updates)
Some features of KeY 1.6 currently unsupported in KeYHeap
- Meta variables, meta variable constraints
- JavaCard transactions, "throughout" modalities
- Test case generation
- Specification extraction
- Correctness proof obligations for taclets
- Proof visualisation, visual debugger
- UML/OCL front end
- Proof reuse
- Eclipse plugin