fmrisc.ProgramExplorer

Class Main

java.lang.Object

fmrisc.ProgramExplorer.Main

public class Main
extends java.lang.Object

Command line interface to the RISC ProgramExplorer

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	copyright
static java.lang.String	version

Constructor Summary

Constructors

Constructor and Description
Main()

Method Summary

Modifier and Type	Method and Description
static void	displayInfo(Task task) Display info (proof) associated to task.
static void	exit(int code) Terminate program with denoted exit code.
static boolean	firstOrder() Return true if first order check is to be applied.
static ErrorStream	getError() Get error stream for printing error messages.
static java.io.File[]	getPath() Get path for looking up source files.
static java.lang.String[]	getProperties() Get the system properties.
static long	getTimeStamp() Get time stamp of current program execution.
static Symbol	getUnit(PackageSymbol top, java.lang.String name, boolean theory) Get symbol of unit denoted by qualified name in top-level package.
static java.lang.String	getVersion() Return version string.
static void	init(TopWindow top) Perform initialization.
static void	internalError(java.lang.String message) Terminate program because of an internal error.
static void	main(java.lang.String[] args) Command line interface to the RISC ProgramExplorer.
static void	processClass(ClassSymbol csymbol) Process class.
static PackageSymbol	processPackages() Process packages as denoted by user path.
static void	processTheory(TheorySymbol tsymbol) Process theory.
static void	proofDone(Proof proof) Called if a proof is completed by the ProofNavigator.
static State.ProverVersion	proverVersion() Return version of default prover.
static void	resetErrors() Reset number of errors to zero.
static void	resetState() Reset system state.
static void	setOutput(java.io.PrintWriter out) Set output stream for printing messages.
static void	setPath(java.io.File[] path) Set path for looking up source files.
static void	setProperties(java.lang.String compileCommand, java.lang.String executeCommand, java.lang.String workingDirectory, java.lang.String mainClass, java.lang.String cvclCommand, java.lang.String cvc3Command, java.lang.String cvc4Command, java.lang.String proverVersion, java.lang.String firstOrder, java.lang.String toLogical) Set the system properties
static boolean	toLogical() Return true if BOOLEAN is translated to LOGICAL.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

version

public static final java.lang.String version

See Also:

Constant Field Values

copyright

public static final java.lang.String copyright

See Also:

Constant Field Values

Constructor Detail

Main

public Main()

Method Detail

main

public static void main(java.lang.String[] args)

Command line interface to the RISC ProgramExplorer. The program reads the following environment variables: PE_CLASSPATH the directories (separated by ":") representing the top package (default the current working directory) PE_CVCL the command for executing the cvcl checker (default "cvcl") 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")

Parameters:

args - command line arguments, see help()

init

public static void init(TopWindow top)

Perform initialization.

Parameters:

top - the top-level window (may be null)

resetState

public static void resetState()

Reset system state.

processPackages

public static PackageSymbol processPackages()

Process packages as denoted by user path.

Returns:

the top-level package (null, if an error occurred).

processClass

public static void processClass(ClassSymbol csymbol)

Process class.

Parameters:

csymbol - the symbol denoting the class.

processTheory

public static void processTheory(TheorySymbol tsymbol)

Process theory.

Parameters:

tsymbol - the symbol denoting the theory.

getUnit

public static Symbol getUnit(PackageSymbol top,
                             java.lang.String name,
                             boolean theory)

Get symbol of unit denoted by qualified name in top-level package.

Parameters:

top - the top-level package

name - the qualified name of the package

theory - true if unit is theory (class, otherwise)

Returns:

the package symbol (or null, if an error occurred)

internalError

public static void internalError(java.lang.String message)

Terminate program because of an internal error.

Parameters:

message - the message indicating the error.

exit

public static void exit(int code)

Terminate program with denoted exit code.

Parameters:

code - the exit code.

getVersion

public static java.lang.String getVersion()

Return version string.

Returns:

the version string.

setOutput

public static void setOutput(java.io.PrintWriter out)

Set output stream for printing messages.

Parameters:

out - the output stream.

getError

public static ErrorStream getError()

Get error stream for printing error messages.

Returns:

the error stream.

resetErrors

public static void resetErrors()

Reset number of errors to zero.

getPath

public static java.io.File[] getPath()

Get path for looking up source files.

Returns:

the path.

setPath

public static void setPath(java.io.File[] path)

Set path for looking up source files.

Parameters:

path - the path.

getProperties

public static java.lang.String[] getProperties()

Get the system properties.

Returns:

an array of 7 elements holding - the compilation command - the execution command - the path of the working directory - the name of the main class - the CVCL command - the CVC3 command - the CVC4 command - the version of the prover (as a string) - TRUE if firstOrder is set - TRUE if toLogical is set

setProperties

public static void setProperties(java.lang.String compileCommand,
                                 java.lang.String executeCommand,
                                 java.lang.String workingDirectory,
                                 java.lang.String mainClass,
                                 java.lang.String cvclCommand,
                                 java.lang.String cvc3Command,
                                 java.lang.String cvc4Command,
                                 java.lang.String proverVersion,
                                 java.lang.String firstOrder,
                                 java.lang.String toLogical)

Set the system properties

Parameters:

compileCommand - the compilation command

executeCommand - the execution command

workingDirectory - the path of the working directory

mainClass - the name of the main class

cvclCommand - the CVCL command

cvc3Command - the CVC3 command

cvc4Command - the CVC4 command

proverVersion - the version of the prover

firstOrder - TRUE if prover is first order

toLogical - TRUE if type LOGICAL is to be used

proofDone

public static void proofDone(Proof proof)

Called if a proof is completed by the ProofNavigator.

Parameters:

proof - the completed proof.

getTimeStamp

public static long getTimeStamp()

Get time stamp of current program execution.

Returns:

the time stamp.

displayInfo

public static void displayInfo(Task task)

Display info (proof) associated to task.

Parameters:

task - the denoted task

firstOrder

public static boolean firstOrder()

Return true if first order check is to be applied.

Returns:

true if first order check is to be applied.

toLogical

public static boolean toLogical()

Return true if BOOLEAN is translated to LOGICAL.

Returns:

true if BOOLEAN is translated to LOGICAL.

proverVersion

public static State.ProverVersion proverVersion()

Return version of default prover.

Returns:

the prover version.