F.1 README
------------------------------------------------------------------------------
README
Information on the RISC ProgramExplorer.
Author: Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>
Copyright (C) 2008-, Research Institute for Symbolic Computation (RISC)
Johannes Kepler University, Linz, Austria, http://www.risc.jku.at
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
------------------------------------------------------------------------------
RISC ProgramExplorer
--------------------
http://www.risc.jku.at/research/formal/software/ProgramExplorer
This is the RISC ProgramExplorer, an interactive program reasoning environment
developed at the Research Institute for Symbolic Computation (RISC). This
software is freely available under the terms of the GNU General Public License,
see file COPYING. The RISC ProgramExplorer runs on computers with
x86-compatible processors under the GNU/Linux operating system. For learning
how to use the software, see the file ~main.pdf~ in the directory ~manual~;
examples can be found in the directory ~examples-ProgramExplorer-CVC3~.
The RISC ProgramExplorer
* provides the overall technological and semantic framework
(programming language and formal specification language),
* translates annotated programs into the semantic model
(programs commands as state relations) which is open
for human investigation,
* generates from the semantic model the verification conditions
which can be semi-automatically proved with the help of
the RISC ProofNavigator, an interactive proof assistant
which is integrated into the RISC ProgramExplorer.
Please send bug reports to the author of this software:
Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>
http://www.risc.jku.at/home/schreine
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University
A-4040 Linz, Austria
A Virtual Machine with the RISC ProgramExplorer
-----------------------------------------------
On the RISC ProgramExplorer web site, you can find a virtual GNU/Linux machine
that has the RISC ProgramExplorer preinstalled. This virtual machine can be
executed with the free virtualization software VirtualBox
(http://www.virtualbox.org) on any computer with an x86-compatible processor
running under Linux, MS Windows, or MacOS. You just need to install VirtualBox,
download the virtual machine, and import the virtual machine into VirtualBox.
This may be for you the easiest option to run the RISC ProgramExplorer;
if you choose this option, see the web site for further instructions.
Running the RISC ProgramExplorer Examples
-----------------------------------------
The installation of the RISC ProgramExplorer contains a subdirectory
~examples-ProgramExplorer-CVC3~ with a number of specified and verified example
programs. To (re)run the examples, go to the directory, unzip the PETASKS.tgz
file and start the RISC ProgramExplorer:
cd examples-ProgramExplorer-CVC3
tar zxf PETASKS.tgz
ProgramExplorer &
Select the tab ~Symbols~ and double-click e.g. on ~Sum~ to see the file
~Sum.java~. Right-click in the ~Symbols~ tab the method ~sum~ and select ~Show
Semantics~ to see the method semantics. Right-click in the ~Tasks~ tab any task
displayed in purple and select ~Execute Task~ to replay the corresponding proof.
Third Party Software
--------------------
The RISC ProgramExplorer uses the following open source programs and
libraries. Most of this is already included in the RISC ProgramExplorer
distribution, but if you want or need, you can download the source code from
the denoted locations (local copies are available on the RISC ProgramExplorer
web site) and compile it on your own. Many thanks to the respective
developers for making this great software freely available!
CVC3 2.4.1
http://www.cs.nyu.edu/acsys/cvc3/
---------------------------------
This is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
problems.
This is the successor of CVCL 2.0 (see below), the RISC ProgramExplorer can
be configured with either versions (but not yet with the newer CVC4 prototype
available from http://www.cs.nyu.edu/acsys/cvc4). To download the CVC3 source,
go the the CVC3 page, click ~Download~ and select the ~Source Distribution~.
CVCL 2.0
http://www.cs.nyu.edu/acsys/cvcl
--------------------------------
This is a C++ library/program for validity checking in various theories.
The RISC ProgramExplorer currently only works with CVCL 2.0, not the newer
CVC3 available from http://www.cs.nyu.edu/acsys/cvc3. To download the CVCL 2.0
source, go to the RISC ProgramExplorer web site (URL see above), Section ~Third
Party Software~, and click on the link ~CVCL 2.0 local copy~.
RIACA OpenMath Library 2.0
http://www.riaca.win.tue.nl/products/openmath/lib
-------------------------------------------------
This is a library for converting mathematical objects to/from
the OpenMath representation.
Go to the link ~OMLib 2.0~ and then ~Downloads~.
Download one of the ~om-lib-src-2.0-rc2.*~ files.
General Purpose Hash Function Algorithms Library
http://www.partow.net/programming/hashfunctions
-----------------------------------------------
A library of hash functions implemented in various languages.
Go to the link ~General Hash Function Source Code (Java)~ to download
the corresponding zip file.
ANTLR 3.2
http://www.antlr.org
--------------------
This is a framework for constructing parsers and lexical analyzers used for
processing the programming/specification language of the RISC ProgramExplorer.
On a Debian 6.0 GNU/Linux distribution, just install the package ~antlr3~
by executing (as superuser) the command
apt-get install antlr3
ANTLR 2.7.6b2
http://www.antlr.org
--------------------
This is a framework for constructing parsers and lexical analyzers used for
processing the logic language of the RISC ProofNavigator.
On a Debian 6.0 GNU/Linux distribution, just install the package ~antlr~
by executing (as superuser) the command
apt-get install antlr
The Eclipse Standard Widget Toolkit 4.3
http://www.eclipse.org/swt
---------------------------------------
This is a widget set for developing GUIs in Java.
Go to section ~Stable~ and download the version ~Linux (x86/GTK2)~ (if you use
a 32bit x86 processor) or ~Linux (x86_64/GTK 2)~ (if you use a 64bit x86
processor).
Mozilla Firefox 3.* or SeaMonkey 2.* (or higher)
http://www.mozilla.org
-----------------------------------------------------
See the question ~What do I need to run the SWT browser in a standalone
application on Linux or Solaris?~ in the FAQ at
http://www.eclipse.org/swt/faq.php.
On a Debian 7.0 GNU/Linux distribution, just install the required Firefox
libraries by executing (as superuser) the command
apt-get install xulrunner-10.0
The GIMP Toolkit GTK+ 2.X (or higher)
http://www.gtk.org
-------------------------------------
This library is required by ~Eclipse Linux (x86/GTK2)~ and by
~Mozilla 1.7.8 GTK2~.
On a Debian 6 GNU/Linux distribution, the package is automatically
installed, if you install the ~mozilla-browser~ package (see above).
On another GNU/Linux distribution, go to the GTK web package, section
~Download~, to download GTK+.
Java Development Kit 7 (or higher)
http://www.oracle.com/technetwork/java/javase/downloads/index.html
------------------------------------
Go to the ~Downloads~ section to download the JDK 7.
Tango Icon Library 0.8.90
http://tango-project.org/
-------------------------
Go to the section ~Base Icon Library~, subsection ~Download~, to download
the icons used in the ProgramExplorer.
------------------------------------------------------------------------------
End of README.
------------------------------------------------------------------------------