******************************************** * KeY Source Code Installation * * Version 0.99.2 * ******************************************** (1) Requirements: ------------------------------------- Operating System: Linux/Unix Java 2 SDK, Version 1.4.x or newer (already installed) For optional UML/OCL support: Together Control Center, Version 6.2 (already installed) Needed additional Libraries: antlr.jar Version >= 2.7.2: parser generator javacc.jar Version >= 3.0 : parser generator dresden-ocl-demo.jar: ocl parser xerces.jar version 1.4.4: used by tudresden.jar recoder.jar version 0.73KeY: a transformation framework for java patched by KeY junit.jar version 3.8.1: test framework jargs.jar log4j.jar Optionally, KeY can make use of the following binaries: ESC Java's decision procedure `Simplify´ Grammatical Framework (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.ps.gz: a short tutorial * KeYDemo_xxx.tgz: example for KeY used in the 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 4) Optional (for UML/OCL support only): Tell the system where the Together Control Center installation is. Do this by setting the environment variable TOGETHER_HOME, e.g. (using csh and Together in ~togetherj/vers6.2/linux) by setenv TOGETHER_HOME ~togetherj/vers6.2/linux 5) (This step is only necessary if you want to make use of the authoring tool Grammatical Framework and/or the decision procedure Simplify.) If you download Simplify not from the KeY-website but elsewhere e.g. directly from Compaq (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 `Simplify´ and `gf´ (Grammatical Framework) 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 6) Change to the subdirectory ./system cd system 7) Compile KeY: make all (or gmake all) As standard Java compiler `jikes´ is the default. If you want to use javac as compiler please use make JAVAC=javac all If you do not have Together, please use one of the following: make keybase make JAVAC=javac keybase (4) Start KeY ------------------------------- Assuming you are still in the `system´ directory, run: ../bin/startkey TogetherCC with the KeY extensions should then start up. For using the KeY prover standalone use: ../bin/runProver If you encounter problems please send a message to support@key-project.org