KeY 1.4.0
KeY 1.4.0 is the current stable release. It was released on March 27, 2009.License
KeY is distributed under the GNU General Public License.Requirements
- Java version 5 or newer
- Supported platforms: Linux, Solaris, Mac OS X, Windows 2000 or above (Windows in bytecode distribution or Java Web Start only)
Download
For getting KeY 1.4.0, choose one of the following options:
- Start it directly via Java Web Start[?] using the "run it now" link on the right
- Download the pre-compiled bytecode version: KeY-1.4.0.tgz or KeY-1.4.0.zip, README-1.4.0.txt, external libraries
- Compile KeY from source: KeY-1.4.0-src.tgz, README-1.4.0-src.txt, external libraries
Additionally, you may want to use:
- External add-ons (Simplify, SMT-LIB provers)
- The following Eclipse plug-in update site, which offers a rudimentary Eclipse integration of KeY:
http://www.key-project.org/download/releases/eclipse
Other versions (no support provided):
- Nightly builds allow access to the latest development versions (also as Webstart - Info)
- A remote site for the latest nightly build of the KeY Eclipse plug-in: http://i12www.ira.uka.de/~bubel/nightly/eclipse/
- Older releases
Examples and Documentation
- A collection of examples (already included in bytecode and sourcecode distribution): examples-1.4.tgz or examples-1.4.zip
- The best source for information on KeY is the KeY Book. In particular, chapter 10 provides a thorough introduction to the system.
- There are several case studies and tutorials
that introduce to the main functions of KeY and show how KeY handles more
extensive contexts. In particular, we recommend the KeY Quicktour as
an introduction.
- A cheat sheet for the KeY-Syntax (draft).
New Features
- Unified proof obligation framework
- sharing of proof obligations across different specification languages
- unified API for adding new proof-obligations
- same GUI elements used for all specification languages
- more elegant translation of old, @pre-like constructs
- Improved JavaCard DL Specification interface
- specification of DL invariants
- Rewrite of JML front-end
- ghost variables/fields and JML set statement
- non_null by default
- \old in loop invariants supported
- \object_creation(type) in JML assignable clauses
- New standalone OCL front-end
- discontinued support for Borland Together integration
- Java language support enhancements:
- enum types (partially)
- inner and anonymous classes
- enhanced for loop
- variable method arguments
- covariant method signature
- Generation of JML specifications
- Strictly pure queries can be pushed directly into an update
- Stable proof loading and saving
- Classpath directive
- Various bugfixes