KeYmaera-release/README.install.bytecode at master · LS-Lab/KeYmaera-release · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
		********************************
		* KeY Byte Code Installation   *
		*        Version 1.5.x         *
		*        Nightly Builds        *
                *     (Development Version)    *
		********************************


(1) Requirements:
-----------------

Operating Systems: Linux/Unix
                   Mac OS X
                   Windows NT, 2000, XP or Vista

Java 2 SDK, Version 1.5.x or newer (already installed)

Needed additional Libraries:
	antlr.jar Version >= 2.7.2: parser generator
	recoderKey.jar
                 a transformation framework for java patched by the KeY group
	log4j.jar

Optionally, KeY can make use of the following binaries:
	ESC Java's decision procedure 'Simplify'
        SMT-LIB provers: bindings exist currently for Yices, CVCLite, CVC3 and SVC
              (export to SMT input file possible)


(2) Contents of the KeY-Distribution
-------------------------------------

  At the KeY-Homepage you can find the following parts:

   * README-xxx.txt: this file
   * KeY-xxx.tgz: the KeY-system in the jar-file version. That is the
                  distribution version without the source code.
   * KeYExtLib_xxx.tgz: contains the external libraries (see above)
   * quicktour_xxx.ps.gz: a short tutorial
   * KeYDemo_xxx.tgz: example for KeY used in the tutorial


(3) Installation (Byte Code)
----------------------------

	1) Copy the KeY-xxx.tgz to a temporary directory;
	   Here: tmp/

	2) Unpack KeY.tgz

		Linux:
		   tar -xzvf KeY-xxx.tgz

		Windows ( use your favorite unpack program that can handle
			  tar-gzipped archives, e.g. WinZip)

	3) The following files should be found in the directory (tmp/):
		setup.jar key.jar LICENSE.TXT

	4) Change to tmp/ and start installation wizard:
               java -jar setup.jar
           ( or (depends on platform): double-click on setup.jar )

	5) Follow the instructions of the wizard.

	6) Optional: Install Simplify and/or SMT-LIB provers.

           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 SMT-LIB provers)


(4) Start KeY
-------------

	Change to the chosen installation directory

	Go to subdirectory bin and run 'startProver' (Windows: 'startProver.bat')


(5) Start KeY in Test Generation Mode
-------------------------------------

	Run 'startProver unit' or if you wish a simpler GUI run 'startProver testing'
	  (Windows: 'startProver.bat unit' or 'startProver.bat testing')

	The library objenesis.jar may be required to run the generated tests.


-------------------------------

If you encounter problems, please send a message to

		support@key-project.org