E. Software Invocation
The shell script ProgramExplorer is the main interface to the program i.e. the program is
typically started by executing
ProgramExplorer &
However, if the script is copied/renamed/linked to ProofNavigator and executed
as
ProofNavigator &
the program starts with a standalone interface to the RISC ProofNavigator [5] (which is part of the
RISC ProgramExplorer).
Invoking the script as
ProgramExplorer -h
gives the following output which lists the available startup options and the environment variables
used:
RISC ProgramExplorer Version 2.0 (November 22, 2012)
http://www.risc.jku.at/research/formal/software/ProgramExplorer
(C) 2008-, Research Institute for Symbolic Computation (RISC)
This is free software distributed under the terms of the GNU GPL.
Execute ~ProgramExplorer -h~ to see the options available.
------------------------------------------------------------------
Usage: ProgramExplorer [OPTION]...
OPTION: one of the following options:
-h, --help: print this message.
-cp, --classpath [PATH]: directories representing top package.
Environment Variables:
PE_CLASSPATH:
the directories (separated by ~:~) representing the top package
(default the current working directory)
PE_JAVAC
the command for compiling java programs (default ~javac~)
PE_JAVA
the command for executing java programs (default ~java~)
PE_CWD
the directory used for compiling/executing
(default the current working directory)
PE_MAIN
the name of the main class of the program (default ~Main~)
PE_CVCL
the command for executing the cvcl checker (default ~cvcl~)
PE_CVC3
the command for executing the cvc3 checker (default ~cvc3~)
PE_CVC4
the command for executing the cvc4 checker (default ~cvc4~)
PE_CHECKER
the initially selected checker (CVCL, CVC3, CVC4)
(default CVC3)
PE_HIGHERORDER
set for higher-order logic (only for CVCL)
PE_BOOLEANFORMULA
set if formula type is BOOLEAN (else LOGICAL)
The command accepts the following startup options:
-
-h, –help
- With this option, the description shown above is printed and the program
terminates.
-
-cp, –classpath Path
- This option expects as Path a sequence of directories separated by
the colon character “:”. The program considers these directories to jointly represent the
root of the package hierarchy; by default, the current working directory (path “.”) alone
represents the root. The directories in Path must not have different class files (extension
.java), theory files (extension .theory), or subdirectories of the same name.
The program uses the values of the following environment variables.
-
PE_CLASSPATH
- If the program is started without the option -cp/–classpath Path,
the value of this variable is considered as the Path, see the description of the option
given above.
-
PE_JAVAC
- The value of this environment variable is considered as the path to the executable
of the Java compiler; by default, the path javac is assumed.
-
PE_JAVA
- The value of this environment variable is considered as the path to the executable
of the Java runtime environment; by default, the path java is assumed.
-
PE_CWD
- The value of this environment variable is considered as the path of the directory
used for compiling/executing respectively creating subdirectories; by the default the
current working directory “.” is used.
-
PE_MAIN
- The value of this environment variable is considered as the name of the main class
of the program to be compiled and executed; by default the value Main is used.
-
PE_CVCL
- The value of this environment variable is considered as the path to the executable
of the Cooperating Validity Checker (CVC) Lite version 2.0; by default, the path cvcl
is assumed.
-
PE_CVC3
- The value of this environment variable is considered as the path to the executable
of the Cooperating Validity Checker Version 3 (CVC3); by default, the path cvc3 is
assumed.
-
PE_CVC4
- The value of this environment variable is considered as the path to the executable
of the Cooperating Validity Checker Version 4 (CVC4); by default, the path cvc4 is
assumed.