------------------------------------------------------------------------------ README Information on the RISC ProgramExplorer. Author: Wolfgang Schreiner 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 . ------------------------------------------------------------------------------ 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 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! CVC4 1.4 http://cvc4.cs.nyu.edu/web/ --------------------------- CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. This is a successor of CVC3 (see below), the RISC ProgramExplorer can be configured with either versions (CVC3 is still default). To download the CVC4 source, go to the CVC4 page, click "Download" and select the "Source tarball". 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. 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. 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 12 "bookworm" GNU/Linux distribution, just install the package "antlr3" by executing (as superuser) the command apt-get install antlr3 The Eclipse Standard Widget Toolkit 4.28 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). WebKitGTK 2.40.2 https://webkitgtk.org/ ------------------------------------------------------------------------ Select the latest version of the "Releases" section. For the builtin "Help" to work properly, WebKitGTK 2.40.2 or newer must be installed; e.g. on a Debian 12 "bookworm" GNU/Linux distribution, just install the package "libwebkit2gtk-4.1-0" by executing (as superuser) the command apt-get install libwebkit2gtk-4.1-0 The GIMP Toolkit GTK3 http://www.gtk.org ----------------------------------- This library is required by "Eclipse SWT Linux". Go to the "Download" section to download GTK3. On a Debian 12 "bookworm" GNU/Linux distribution, just install the package "libgtk-3-0" by executing (as superuser) the command apt-get install libgtk-3-0 In the shell script "ProgramExplorer", set the variable SWT_GTK3 to 1. Java Development Kit (Oracle JDK 17 recommended) http://www.oracle.com/technetwork/java/javase/downloads/index.html ------------------------------------------------------------------ Go to the "Downloads" section to download the JDK. Oracle JDK 17 is recommended, OpenJDK 17 is an alternative. Later versions should also work but have not been tested. 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. ------------------------------------------------------------------------------