------------------------------------------------------------------------------ README Information on RISCAL. Author: Wolfgang Schreiner Copyright (C) 2016-, 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 Algorithm Language (RISCAL) ================================ http://www.risc.jku.at/research/formal/software/RISCAL This is the RISC Algorithm Language (RISCAL), a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation. RISCAL also includes an interface to various SMT solvers and provides (via an embedding of the RISCTP theorem proving interface) theorem proving capabilities. This software has been developed at the Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University (JKU) in Linz, Austria. It is freely available under the terms of the GNU General Public License, see file COPYING. RISCAL runs on computers with x86-compatible processors supporting Java and the Eclipse Standard Widget Toolkit (SWT); it has been developed and tested on a computer with the GNU/Linux operating system and a x86-64 processor. For learning how to use the software, see the file "main.pdf" in the directory "manual"; examples can be found in the directory "spec". Please send bug reports to the main 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 The SMT extension has been developed by Franz-Xaver Reichl The LTL model checker has been developed by Ágoston Sütő A Virtual Machine with RISCAL ============================= On the RISCAL web site, you can find a virtual GNU/Linux machine that has RISCAL 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 MacOSx. You just need to install VirtualBox, download the virtual machine, and import the virtual machine into VirtualBox. The virtual machine runs a 64-bit operating system and thus requires from your computer hardware support for virtualization (Intel VT-x or AMD-V); it may be necessary to enable this support in the BIOS of your computer. This may be for you the easiest option to run the software; if you choose this option, see the web site for further instructions on how to get the virtual machine. After installation and login as "guest" you have the command RISCAL & The Distribution ================ The distribution has the following contents: README ... this file COPYING ... the GNU General Public Licence Version 3 CHANGES ... the version history of the software etc/ RISCAL ... the execution script run* ... examples of server execution scripts boolector ... Boolector (GNU Linux/x86-64 executable) cvc4 ... CVC4 (GNU Linux/x86-64 executable) cvc5 ... cvc5 (GNU Linux/x86-64 executable) vampire ... Vampire (GNU Linux/x86-64 executable) yices-smt2 ... Yices 2 (GNU Linux/x86-64 executable) z3 ... Z3 (GNU Linux/x86-64 executable) lib/ *.jar ... the Java compiled libraries swt64/swt.jar ... the SWT library for GNU/Linux and x86-64 processors doc/ main.pdf ... the manual spec/ *.txt ... sample specifications src/ */*.java ... the Java source code Installation ============ First make sure that you have installed the third party software described below (Java Development Kit is required, JavaFX and WebKitGTK are optional). Then copy file etc/RISCAL to a directory in your PATH and adapt in this file the variable JAVA to point to the Java executable "java" of your JDK. Adapt LIB to point to the directory "lib" of the RISCAL distribution and make sure that the subdirectory $LIB/swt64 contains the SWT library intended for your operating system and processor. Also configure the graphical user interface options via the environment variables described in this file. You should then be able to execute RISCAL & You may configure by the environment variables "RISCALFontDefault" and "RISCALFontMethod" the names of the fonts to be used in the input/output areas respectively the method menu. Third Party Software That You Have to Install ============================================= RISCAL assumes that the following third party software is installed on your computer (if it is not already provided by your GNU/Linux distribution, you have to downlad and install it manually). 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. For the (optional) use of the visualization features of RISCAL, Oracle JDK respectively OpenJDK also need an installation of JavaFX. JavaFX (OpenJFX 17 recommended) https://openjfx.io/ https://gluonhq.com/products/javafx/ ------------------------------------ Select "Include older versions" and press the "Download" button to download the appropriate version of the library. JavaFX is a framework for graphical user interfaces. It is only needed if RISCAL is started with the command line option "-visual" to enable the visualization of the execution traces of procedures and of the evaluation of formulas. JavaFX is not part of the Oracle JDK/OpenJDK distribution; it has to be downloaded and installed separately. On a Debian 12 "bookworm" GNU/Linux distribution, the older version JavaFX 11 can be installed as package "openjfx" by executing (as superuser) apt-get install openjfx WebKitGTK 2.44.2 https://webkitgtk.org/ ---------------------- Select the latest version of the "Releases" section. For the builtin "Help" to work properly, WebKitGTK 2.44.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 Third Party Software That Comes with RISCAL =========================================== RISCAL also uses the the following open source software developed by third parties. This software is already included in the distribution, but if you want or need, you can download the source code from the denoted locations and compile it on your own. Many thanks to the respective developers for making this great software freely available! The Eclipse Standard Widget Toolkit 4.32 http://www.eclipse.org/swt ---------------------------------------- This is a widget set for developing GUIs in Java. Go to section "Stable" and download the version "Linux (64 bit version)" (if you use Linux with a 64bit x86 processor). NOTE: in SWT version 4.32, the library file "swt.jar" downloaded according to above procedure does not work, because it is signed with an invalid signature. Download instead the Eclipse 2024-06 package for your architecture and use from directory "eclipse/plugins" the file with name pattern "org.eclipse.swt.*.jar" (e.g., on a Linux system with a 64bit x86 processor, this name pattern is "org.eclipse.swt.gtk.linux.x86_64_*.jar"). Eclipse GEF/Zest 5.4.0 https://www.eclipse.org/gef --------------------------- This is a framework for visualizing graphs. It is only needed if RISCAL is started with the command line option "-visual" to enable the visualization of the execution traces of procedures and the evaluation of formulas. Go to the "Download" link and download the "5.4.0" build. ANTLR 4.13.0 http://www.antlr.org -------------------- This is a framework for constructing parsers and lexical analyzers used for processing the programming/specification language of RISCAL. Go to the "Download" section to download the latest 4.* version of the library. On a Debian 12 "bookworm" GNU/Linux distribution, just install the package "antlr4" by executing (as superuser) the command apt-get install antlr4 Tango Icon Library 0.8.90 http://tango.freedesktop.org ---------------------------- This library provides the button/menu icons used by RISCAL. Go to the section "Base Icon Library", subsection "Download", to download the library. Boolector 3.1.0: https://boolector.github.io/ CVC4 1.7: https://cvc4.github.io/ cvc5 1.1.2: https://cvc5.github.io/ Vampire 4.7: https://vprover.github.io/ Yices 2.6.1: https://yices.csl.sri.com/ Z3 4.13.0: https://github.com/Z3Prover --------------------------------------------- To use the SMT respectively TP extension, at least some of these SMT solvers respectively theorem provers have to be installed (above versions have been tested, other versions may or may not work). The RISCAL distribution is bundled with GNU Linux/x86-64 executables of these solvers. ------------------------------------------------------------------------------ End of README. ------------------------------------------------------------------------------