Basic Usage of SPARK Ada

• If using Linux Machines in the Linux Lab
  • Please follow the instructions for Setting up Linux Lab machines using SuSe for use with Spark Ada.
  • Please study the page Basic Terminology in Linux explaining the basic terminology of Linux such as directory, ~/bin etc.
• Examples from the lectures can be found here
• It is very important that you create for each project a new directory.
  A project could be for instance coursework_1_a (for coursework 1 (a) - please note that that you shouldn't use blanks, brackets, since that may cause problems with Spark Ada).
  
  • The reason is that SPARK ada will when using the standard main.gpr file check all files in the current directory and no files in any other directory.
    • The main.gpr file can be found in lib/main.gpr in the git repository.
    • You can use as well a mainWithoutRangeCheck.gpr file found as well in lib - SPARK Ada will not create verification conditions referring to range conditions when this file is used.
• You can create directories by using the file manager.
• The easiest is to copy using the file manager files from an existing project to your new project.
• Note: File names need to be in lower case, and should start with a (lower case) letter.
• Your project normally should have .ads and .adb files and a file main.gpr. I always use the same file, namely lib/main.gpr as found in the git repository.
• The recommended way is to then only open gnatstudio from the file manager by left click on the file main.gpr.
  • I highly recommend to open gnatstudio only using this method
  • This method guarantees that the files you see on the left pane are all files which will be checked when running checks by Spark Ada.
  • If you open other files, e.g. .ads or .adb files directly in gnatstudio, it very often occurs that gnatstudio displays files, which it doesn't check (e.g. because they are not in lower case).
• The recommend way is to only open files under gnatstudio using the left side menu under Main and clicking on the first folder icon with a ".". Open the files from there.
• This guarantees that only files associated with your project and visible to SPARK Ada are opened.
• If you open a file in any other way, when using SPARK Ada it may not be checked even though that file is currently open.
• Especially I don't recommend to open files using the top menu File.
• If you add, delete or edit any files without using gnatstudio it is recommended to close gnatstudio and start it again.
• Commands of gnatstudio I have been using
  • For checking the syntax (only Ada not SPARK Ada)
    
    Build → Check Syntax
    
    
  • For compiling all ada files in a directory use
    
    Build → Project → Build All
    
    • This will generate files which can than be linked to othe projects. It will not create executable files.
      The main purpose for use this command in the labs is to check that the files are correct ada files.
  • For compiling an executable file (i.e. with input/output)
    Click on the executable .adb file, make sure that it is shown and the active tab, and then use
    
    Build → Project → Build < current file >
    
    You need to have a adb file open which has no package and only one procedure with the same name as the file and with no arguments.
  • For running an executable file use
    
    Run → Custom
    
    
    • Under Windows use the option "run in an external terminal" which will open a command shell. From there you can run the program which is usually called main.exe.
    • Under Linux
      • You should have set up in preferences (edit → preferences → External commands → on right side change "xterm -hold -e" to "xterm -hold".
        • Make sure the - is as the - you get from the keyboard (copying from a webpage might result in a different character)
      • After setting it up when you execute Run → Custom
        the command "xterm -hold" should be shown.
      • Now you click on both "Run in executables directory" and "Run in an external terminal".
        • In case your executable file is not main.adb but myfile.adb type in ./myfile
      • You can keep that terminal open and use it for executing the executable again later.
  • Commands for running SPARK Ada checks
    • SPARK → Examine All
      
      Runs data flow and examination flow analysis
    • SPARK → Prove all
      
      I use as proof stragegy in the following menu "Progressively Split" (3rd option)
      Runs all 3 levels of SPARK Ada including verification conditions.

Usage of Why3 (only on Linux)

• Why3 will be installed later (so please come back once it is installed)
• Please note that why3 will not be used for lab tasks 2021/22, but we might have a demo so that you see how it works.
  • Once you have verified programs involving verification conditions, you can use the why3 file as explained in
    Basic Usage of Why3

Using SPARK Ada from the Command Line (Linux)

• On Linux machines you can run as well SPARK Ada from the command shell.
  The commands I am using are
  • gnatmake file.adb
    For compiling file.adb
    Most of the times we will not create complete programs which can be executed, then this command will only create linkable files which cannot be executed, and this command is usually not needed.
  • gnatprove -P main.gpr --mode=flow
    Runs data flow and examination flow analysis (for project containg main.gpr).
  • gnatprove -P main.gpr --proof=progressive
    Runs all 3 levels of SPARK Ada including verification conditions.
    • You can use as well a mainWithoutRangeCheck.gpr file - SPARK Ada will not create verification conditions referring to range conditions when this file is used.