CP SC 872

 

The Resolve Compiler/Verifier

This web page introduces the Resolve analyzer and explains how it should be used. It contains the following sections:

  • The Resolve Compiler/Verifier and What It Can Do
  • Requirements and Downloads
  • Windows and Unix Path Set up
  • Running the Analyzer/Compiler/Verifier
  • Directory Structure and Conventions
  • Translating Mathematical Symbols to Text
  • Notes and Errata
  • Feedback

The Resolve Compiler/Verifier and What It Can Do

The Resolve analyzer is the front end of a compiler for the Resolve language.  Click here for the grammar.  The current version translates Resolve files to Java, reporting the same kinds of errors a compiler would report.  It will also generate verification conditions for a limited class of implementations.

The current version of the analyzer can translate a class of Resolve files and type-check programming expressions; a version that type-checks mathematical expressions is expected to be available shortly. Because the analyzer is incomplete, it may incorrectly pass a file that should have failed analysis, but it should never fail a file that should have passed analysis.

The analyzer is still the beta stage of development, so if you have a file that you think is correct but failed analysis, please report it to murali@cs.clemson.edu.

Requirements and Downloads

  • You need to have Java version 5.0 or higher installed on your machine to run the translator.  To find the current version of Java on your machine, use the command “java –version” in the command prompt window. 
  • Jar files to download: antlr.jar and Resolve08.jar.  (Note that you should use Resolve08.jar in the paths as given in the instructions on where to place these files.)
  • Limited library to download: workspace.zip. Put this into a directory (or folder) of your choice, say, Resolve, and click “extract here” when you unzip it.  Unzipping will create directory workspace and subdirectories. 

Unix Set up (recommended)

  • On a Unix system, type java and javac in your current directory to check that they are available for your use.
  • Copy the jar files to your working directory. 
  • Change the Java CLASSPATH as shown below, supposing Resolve is your current directory and $ is the prompt (without any blank spaces except for one immediately after CLASSPATH or line breaks): $ setenv CLASSPATH .:/users/murali/Resolve/Resolve08.jar:/users/murali/Resolve/antlr.jar:/users/murali/Resolve/workspace
  • To avoid repeating the above step everytime, you might want to create a file env in your directory with the above setenv command and then just type: $ source env
  • If you are using bash, you need to use a different command to set up the environment.  It is: export CLASSPATH=.:/users/murali/Resolve/Resolve08.jar:/users/murali/Resolve/antlr.jar:/users/murali/Resolve/workspace
  • Warnings: Be sure to avoid punctuation errors when entering path information.   If you get the error, Exception in thread "main" java.lang.NoClassDefFoundError, it is probably a path declaration error.  If not, check for typos in your commands carefully.

Windows Set up 

  • On a Windows system, suppose that jre1.5.0_06 is the current version and it is at C:\Program Files\Java\jre1.5.0_06.  Then place the two jar files in the directory – C:\Program Files\Java\jre1.5.0_06\lib\ext, i.e., under the lib\ext of the current version.  If you put these files elsewhere, you may need to add them to the system Path and CLASSPATH variables (see below) as appropriate.  Sometimes, Windows insists on calling these downloads antlr.zip and Resolve08.zip, respectively.  If that is the case, simply rename them as .jar files or include the .zip extension instead of .jar extension in the paths.
  • Find the System Properties window by clicking on System in the Control panel; note that System may be under Hardware.  Find and select Environment Variables under the menu “Advanced”, for example.  
  • Find and select the User (not System) Path variable and click on “Edit”.  Add to the end, your Java information and the library location  (the leading semicolon is only necessary if you have other entries in your path):  ;C:\Program Files\Java\jre1.5.0_06\bin; C:\Program Files\Java\jre1.5.0_06\lib; C:\Documents and Settings\murali\My Documents\Resolve\workspace
  • Click OK to the above.  Find and select the User (not System) CLASSPATH  variable and click on “Edit”.  Add to the end (note the leading semicolon), the location of your limited library, for example: C:\Documents and Settings\murali\My Documents\Resolve\workspace
  • Click OK to the above.  It may be necessary to include the current directory in your CLASSPATH; this can be done by adding editing the environment variables and adding “.”, the current directory to the path, for example : ;.
  • Click OK to the above.  On some systems, under Environment Variables, it may be necessary to select and change the System Path and System CLASSPATH variables, and add the location of your limited library, for example: C:\Documents and Settings\murali\My Documents\Resolve\workspace
  • Click OK and close the System Properties window. 
  • Warnings: Close the command prompt window and reopen it for the paths to take effect.  You may also need to log out depending on your path changes.  Be sure to avoid double semicolons, or blank spaces after semicolons when entering path information.   If you get the error, Exception in thread "main" java.lang.NoClassDefFoundError, it is probably a path declaration error. If not, check for typos in your commands carefully.

 

.

Running the Compiler and Verifier

  1. Go to the directory that contains the file you want to compile, e.g., cd into the Stack_Examples directory and run the analyzer on Alt_Rev_Stack.fa:

    $ cd C:\Documents and Settings\murali\My Documents\Resolve\workspace\RESOLVE\Main\Facilities\User\Stack_Examples
    $ java edu.clemson.cs.r2jt.Main –translate +bodies Alt_Rev_Stack.fa

  1. Compile the generated java file using your Java compiler: 
$ javac Alt_Rev_Stack.java
 
  1. Run the java program, that takes 4 numbers and prints them out in reverse order using a Stack: 
$ java Alt_Rev_Stack
 
  1. The current Resolve compiler does not automatically compile all necessary files, so you may have to compile each Resolve file separately on your own.  Otherwise, the Java compiler will be missing files it needs. 
$ java Alt_Rev_Stack
  1. The verifier is currently limited to handling enhancements. To generate verification conditions for a Stack Reverse operation, cd into the Stack directory and run the verifier on Obvious_Rev_Realiz.rb:

    $ cd C:\Documents and Settings\murali\My Documents\Resolve\workspace\RESOLVE\Main\Concepts\Stack
    $ java edu.clemson.cs.r2jt.Main –split Obvious_Rev_Realiz.rb

  1. The generated VC’s are found at Obvious_Rev_Realiz.asrt.  Other enhancement examples may be found under directory Queue or under \Concepts\Standard\Integer

Directory Structure Assumptions and Conventions

When you run the analyzer on Stack_Template.co, it assumes that a directory named Main exists above the level of Stack_Template.co. It will look in the directory tree defined by Main for any files that Stack_Template.co depends on; it will not look outside of Main. Place modules in directories according to the following rules:

  • Math Units (*.mt files), Concepts (*.co files), and Facilities (*.fa files) can appear anywhere beneath Main
  • Realizations (*.rb files) and Enhancements (*.en files) must appear in the same directory as their associated Concept.

The conventional directory structure below Main is: 

                     Main
                      |
     +----------------+------------------+
     |                |                  |
 Math_Units       Facilities          Concepts
                                         |
                                 +-------+------+--->>>
                                 |       |      |
                               Stack   Queue   List

where Stack, Queue, and List are example directories used to illustrate the fact that each concept gets its own directory.

Translating Mathematical Symbols to Text

The modules in the course notes are written using mathematical symbols. Perhaps someday we will have a fancy editor for the Resolve language that allows one to type in mathematical symbols - perhaps. For now, all input files to the analyzer must be text only. Compare Stack_Template and Array_Realiz in the course notes with Stack_Template.co and Array_Realiz.rb in the Main/Concepts/Stack directory. This should give you enough information about the symbol-to-text translation to allow you to complete project #1.

Examples:

The text version of the correspondence clause for an Array_Realiz is:

    correspondence Conc.Q = (Concatenation i: Integer
        where 1 <= i <= Q.Last,
        <Q.Contents(i)>);

Note that the parentheses around the concatenation expression are mandatory.

Notes and Errata

  • NEW To write the main procedure in the top level facility, use the following outline:

Facility Stack_Queue_User_Facility;

    (* Facility declarations go here. *)

    Operation Main();
    Procedure
        (* Variable declarations and procedure body go here. *)
    end Main;

end Stack_Queue_User_Facility;

  • Remember that parentheses are mandatory around Concatentation expressions.
  • To assign a truth value to a boolean programming variable, use the operations True() and False() found in Boolean_Template. For example, to assign a value of true to the variable x, write:

    x := True();

  • The keywords constraints and conventions may be singular or plural - the analyzer does not discriminate between the singular and plural forms.
  • In a Type declaration, the keyword phrase is represented by may be replaced with an equal sign (=).
  • The specification of Defensive_Push is given on page 42 of the class notes. Here is the specification in text:

Operation Defensive_Push(alters E: Entry;
                         updates S: Stack;
                         replaces full_flag: Boolean);
    ensures (if |#S| < Max_Depth then S = <#E> * #S
             and not full_flag) and
            (if |#S| = Max_Depth then full_flag);

  • There is a discrepency between the course notes (Figure 6 on page 67) and the current version of the analyzer. In the notes a procedure can be distinct from an operation within the same facility:

    Operation Copy_Integer(replaces C: Integer;
                           preserves Orig: Integer);
        ensures C = Orig;

    -- Any amount of code can go here --

    Procedure Copy_Integer(replaces C: Integer;
                           preserves Orig: Integer);
        C = Replica(Orig);
    end;

In the current version of the analyzer, however, the operation and procedure must be combined:

    Operation Copy_Integer(replaces C: Integer;
                           preserves Orig: Integer);
        ensures C = Orig;
    Procedure
        C = Replica(Orig);
    end;

Notice that in the second version, neither the operation name nor the parameters are repeated on the line beginning with Procedure. Your code should comform to the later construction to pass analysis. Future versions of the analyzer will support both constructions.

Feedback

Please direct any feedback regarding the RESOLVE analyzer or the RESOLVE language to murali@cs.clemson.edu. All feedback is welcome: possible bugs in the analyzer, confusing error messages, confusing language syntax, obscure keywords.