Download KeY-Hoare

KeY-Hoare is built on top of the software verification tool KeY and features a Hoare calculus with updates. It is used in the Chalmers undergraduate course Program Verification to teach the Hoare calculus.

License

KeY is distributed under the GNU General Public License.

Requirements

• Java JDK 1.8.0 or newer. Supported platforms: Linux, Solaris, Windows 2000 or above (Windows in bytecode distribution only), MacOSX.

Features

• partial correctness proofs
• total and execution time correctness proofs (version >=0.1.6)
• integer and boolean typed arrays (version >=0.1.7)

Documentation and Examples

• A paper explaining the implemented Hoare calculus including a brief reference manual is here.
• Selected examples for download. More examples are currently only available on request.

Installation

For our students we recommend strongly to use either the webstart install (easiest) or the provided binary distribution.

Webstart (easiest): When you have installed the Java plug-in for your browser, clicking on start KeY-Hoare should be sufficient (you need to accept/trust the certificate) and no further action is necessary. If you have not installed the Java plug-in you can use Webstart via the command line command:

javaws http://i12www.iti.kit.edu/key/download/hoare/download/webstart/KeY-Hoare.jnlp
After the first download, webstart will allow you to start KeY-Hoare even when you are offline. Therefore execute javaws, select KeY-Hoare in the offered list and press the button Start Offline.

Binary Distribution: Copy the zipped file to any place and unzip it. You should now find the directory KeY-Hoare-0.1.10. Execute the program startKeYHoare(Linux or MacOSX) resp. startKeYHoare.bat(Windows). You may also just double click (depending on your Java installation) the file key.jar, but the scripts mentioned before assign more memory to the JVM. So if you run into OutOfMemory errors, try the scripts instead.

In order to install and compile the source code distribution, please follow the instructions given in the linked README file.

Download

• Use Java Webstart and launch KeY-Hoare with one click (you need to accept/trust the certificate): Start KeY-Hoare
• Get the pre-compiled bytecode version: KeY-Hoare-0.1.10.zip 
• Source Code version: KeY-Hoare-0.1.10-src.tgz (README)
  • Source-Download required external libraries (use those for KeY-1.6.0)

Known Issues

• The current version uses a Java AST in order to embed the used while language. In future version there will be a native support of the programming language.
• Further glitches are due to the simulation of a Hoare calculus using a sequent calculus for dynamic logics. Future versions will reduce the glitches to a minimum supporting native parsers for the used fragment.