********************************* * KeY Source Code Installation * * Version 2.0.2 * ******************************** (1) Requirements: ------------------------------------- Operating System: Linux/Unix, MacOSX, Windows (untested) Java SE 6 or newer (already installed) Needed additional Libraries: antlr.jar Version >= 2.7.2: parser generator javacc.jar Version >= 3.0 : parser generator recoderKey.jar a transformation framework for java patched by the KeY group Optionally, KeY can make use of the following binaries: SMT Solvers: bindings exist currently for Z3, Simplify, Yices and CVC3 (export to SMT input file possible) (2) Contents of the KeY-Distribution ------------------------------------- At the KeY-Homepage you can find the following parts: * README.xxx-src.txt: this file * KeY-xxx-src.tgz: the source code version of KeY-system * KeYExtLib_xxx.tgz: contains the external libraries * quicktour_xxx.zip or quicktour_xxx.tgz: a short tutorial (3) Installation (Source Code) ------------------------------------- 1) Untar the tar-gzipped file: tar -xvzf KeY-xxx-src.tgz 2) Change to the created directory key-xxx cd key-xxx 3) Install the needed libraries. Use the environment variable $KEY_LIB to point to the directory the needed libraries are in. If you use csh and all the needed libraries are in ~/key_lib use, e.g. setenv KEY_LIB ~/key_lib or (bash) export KEY_LIB=~/key_lib or (Windows) set KEY_LIB= 4) Optional: Install Simplify and/or other SMT solvers. If you download Simplify not from the KeY-website but elsewhere (e.g. as part of ESC/Java), follow the intallation instructions given there. Then rename the Simplify binary which could be named something like Simplify Simplify-1.5.4.linux (Linux version) or Simplify-1.5.4.exe (Windows) to just 'Simplify' resp. 'Simplify.exe'. When using Linux make sure that the file is is executable (you can make a file executable by issuing the command 'chmod a+x filename'). Make sure that the path where the binaries reside is included in your PATH environment variable or in the KEY_LIB environment variable. If not, use (e.g., in the csh to include Simplify which is assumed to be located in ~/simplify): setenv PATH ~/simplify:$PATH In bash-syntax the above command is export PATH=$PATH:~/simplify (analog procedure for other solvers) 5) Change to the subdirectory ./system cd system 6) Compile KeY: make all (or gmake all) or export ANT_OPTS="-Xmx512m" ant (compilation via 'ant' should work under Windows too, but you need to set the ANT_OPTS environment variable most likely via set ANT_OPTS = "-Xmx512m" ) (4) Start KeY ------------------------------- Assuming you are still in the 'system' directory, run: ../bin/runProver ------------------------------- If you encounter problems, please send a message to support@key-project.org