Come to the EDS Software Verification and Testing Laboratory (101 SEB) located in the Science and Engineering Building. This lab has eight computers with Microsoft NT 4.0 operating system installed, and Solaries based server for Dial In Services.

• Click on the Command Prompt Icon
• Using the DOS Command, Switch to Working Subdirectory

  Example :
  cd A:\my_dir   or   cd yourdirectory\...

Now you are able to invoke the SPARK System. Spark System comprises of three parts:

1. Spark Examiner -> this is a separate program that examines the supplied source code and analyses it, specifically against the annotations supplied by the programmer.

2. Spark Simplifier -> executable GUI that simplifies and proves, if it can, the verification conditions created by the Spark Examiner.

3. Spark Proof Checker -> supplies rules, laws, etc, to enable the user to prove, in an interactive way, the verification conditions which were too complicated to be proved by the Spark Simplifier.

1. First, run the Spark Examiner. To invoke the Spark Examiner, first change into the local subdirectory (a subdirectory where the source code is located, example: a:\my_directory\), then type “spark /vcs my_file_name.ada” where my_file_name is the name of source code supplied by you and the “/vcs” is a switch that will tell the Examiner to produce the verification conditions. Examiner will examine your code and produce a report about this file. Any information about this file can be found in the my_file_name.lst. Open it to see the results.

   
   

   Note, Spark will look for the submitted file only in the working/current subdirectory. If the file isn't there, Examiner will issue a message "File not Found!" and terminate.

   
   

   File correctly submitted to the Examiner will be analyzed, and as the final result Spark Examiner will create a file listing 'my_file_name.lst' where 'file correctnes' result can be found. In addition to the file listing, for each procedure/function in analized package, Spark Examiner produces Verification Conditions. Verification Conditions are located in a subdirectory named after the package name. This subdirectory is created automatically by the Spark Examiner. Created file(s) have '.vcg' file extension.

2. Second, run the Spade Simplifier. Using the DOS Command 'cd' (change directory), change into subdirectory created in the step above. To invoke Spade Simplifier type 'Simp', then press the return key. In about 15-20 seconds Open Dialog Box will appear asking 'Simplify which file?'. Select one of the files (by clicking on it), then press the 'Open' button.

   Simplifier, using the built-in logical rules, tries to prove or at least simplify submitted Verification Conditions.

3. Third, run Spade Proof Checker. In the same subdirectory type 'checker'. This command invokes the Proof Checker. As in the case of the Simplifier, an Open Dialog Box apppears asking 'Prove which VC?'. The default file extension is '.siv', however, a user also is allowed to submit to the Spade Proof Checker a file with the '.vcg' extension as well. Select one of the files (by clicking on it), then press the 'Open' button.

• In order to use the dial in services, a student taking CSE 438/538 Course has to have a valid account on Perlis (It is the server for the SECS Domain). If a student doesn't have one, he/she is to submit a valid vela accout (an OU email address) to Professor Laski. Then an account will be created for that student within 1 - 2 days.

• If a valid Perlis account exists, you must do the following before using Spark systems.

  • First, logon to the eds-testing-lab (telnet eds-testing-lab.secs.oakland.edu), then using one of the UNIX editors (vi, emacs, pico, etc.) edit your '.cshrc' file. Be very careful. If you had never before used UNIX nor had you used any of the UNIX editors, ask for assistance!

    Here are the lines that you have to add to your '.cshrc' file
    

    set path=($path /local/spark-5.0/spark )

    setenv LM_LICENSE_FILE /local/lmgrd/license.dat

    source /local/spark-5.0/poplog/poplogin

    source /local/spark-5.0/simplifier/saslogin

    source /local/spark-5.0/checker/chklogin

  • Second, recompile the '.cshrc' file by typing 'source .cshrc'
  • Third, test if it works:
    • To invoke the Spark Examiner type
      spark filename.ada
    • To invoke the Spade Simplifier type
      spadesimp filename.vcg
    • To invoke the Spade Proof Checker type
      checker filename.siv