Using the RESOLVE Compiler/Verifier from the Command Line


Common RESOLVE Compiler/Verifier options

-translate +bodies used to create Java source files
-vcs used to generate verification conditions
-vcs -quickprove used to prove a subset of the generated VC's **
-vcs -isabelle used to generate VC's compatible with the Isabelle proof assistant


Compiling with RESOLVE

This section begins with a demonstration of how to compile the example facility Alt_Rev_Stack.fa, using the Command Prompt in Windows Vista. For instructions on how to use the Eclipse IDE and RESOLVE plugin click HERE. With the exception of the cd (change directory) command, all of the steps will work with Unix/Linux systems as well. The compiler will use this file to create a Java program that will take 4 integers from the command line, store them in a stack, and print out the stack in reverse order. The first step is to use compile Alt_Rev_Stack.fa using RESOLVE. Enter the following commands at the prompt.

cd C:\Users\resolve\Downloads\workspace\RESOLVE\Main\Facilities\Users\Stack_Examples\

java edu.clemson.cs.r2jt.Main -translate +bodies Alt_Rev_Stack.fa


The first command changes the directory to location of the example file and the second invokes the compiler. Once the facility has been compiled, the newly created Java file (Alt_Rev_Stack.java) is ready to compiled with the Java compiler using the command:

javac Alt_Rev_Stack.java


Currently the RESOLVE compiler does not automatically compile all the required concept files, so it is likely that the Java compiler will complain and list a bunch of errors at this point. The screen shot below shows the errors in this example.



By examining the errors, the missing concept files can be indentified:

Stack_Template.co
Obvious_Reading_Realiz.rb
Reading_Capability.en
Obvious_Writing_Realiz.rb
Writing_Capability.en
Init_Array_Realiz.rb

Once the missing files have been identified, they need to be RESOLVE compiled so that the Java compiler has what it needs to create the program. Use the following commands to change to the stack concept files directory and compile the concepts:

cd ../../../Concepts/Stack

java edu.clemson.cs.r2jt.Main -translate +bodies Stack_Template.co

java edu.clemson.cs.r2jt.Main -translate +bodies Obvious_Reading_Realiz.rb

java edu.clemson.cs.r2jt.Main -translate +bodies Reading_Capability.en

java edu.clemson.cs.r2jt.Main -translate +bodies Obvious_Writing_Realiz.rb

java edu.clemson.cs.r2jt.Main -translate +bodies Writing_Capability.en

java edu.clemson.cs.r2jt.Main -translate +bodies Init_Array_Realiz.rb


Now that all the necessary files have been compiled, use the following commands to change back to the example directory and run the Java compiler:

cd ../../Facilities/User/Stack_Examples

javac Alt_Rev_Stack.java

If there aren't any errors at this point, the example program is ready to test. Use the java command to run the program:

java RESOLVE.Main.Facilities.User.Stack_Examples.Alt_Rev_Stack


Enter four integer values, they can be on the same line separated by spaces or each can be entered separately followed by the enter key. After the fourth integer has been entered and the enter key is pressed, they should be printed to the command prompt in reverse order, as seen below:



RESOLVE Verification

To generate and prove verification conditions for a file, navigate to the Unbounded_Stack concepts directory and run the verifier on Obvious_Flip_Realization.rb. This file was chosen over Alt_Rev_Stack.fa because it uses Modified_String_Theory and can be proven using the automated prover. Start by entering the following commands in the Command Prompt.

cd ../../../Concepts/Unbounded_Stack

java edu.clemson.cs.r2jt.Main -vcs Obvious_Flip_Realization.rb


The generated VC's are found at Obvious_Flip_Realization.asrt. The verification conditions generated by RESOLVE for Obvious_Flip_Realization.rb are seen below. Any issues with VC generation can be directed to Heather Harton at Clemson University.



RESOLVE Automated Proving

The RESOLVE Compiler/Verifier can also be used to automatically prove the VC's using the -vcs -prove command line arguments. See the screen shot below for the output from the automated prover.



Notice that the last lines of the output state that the RESOLVE was able to prove all three of the generated verification conditions. Contact Hampton Smith at Clemson University about any problems with the automated prover. The last choice on the list of common options uses the -vcs and -isabelle flags. Using the -isabelle flag makes the compiler generate the verification conditions in a format that is compatible with the Isabelle proof assistant. Isabelle VC's will be created and saved using the -thy extension.

For more information, check out the Documentation Page.

Page last updated by Chuck Cook on June 30, 2009.