Frequently Asked Questions on SPARK Ada (Lecture CSCM13/CSC313, Swansea)

• When checking my program with SPARK Ada some files don't get checked?
  • Do you have any SPARK Ada file names having upper case letters or starting with a digit? All of these files will be ignored by SPARK Ada.
  • Your files need to start with the line
    
    pragma SPARK_Mode;
    
    or some other statement which turns SPARK Ada checking on.
  • Many instructions of spark ada work if there are no blanks in the path towards your files.
• Last time I checked my files and everything was checked as being okay. Now this is no longer the case.
  • Check the first question "When checking my program with SPARK Ada some files don't get checked?" above.
• How do I compile and run your SPARK Ada programs?
  • See compilingAndRunningPrograms.html
• How do I install why3 on my Windows machine?
  • The main website about installing why3 is https://www.lri.fr/~marche/MPRI-2-36-1/install.html
  • It says "In case you are still using Windows, install Ubuntu either in a virtual machine (using e.g., VirtualBox), or on a USB stick (using e.g., LinuxLive USB creator), or on a separate partition in parallel of Windows (using e.g., Wubi). You'll save yourself a lot of trouble."
  • I recommend to try whether you can running Ubuntu or some other Linux version via a USB stick (so without installing it on your machine) and then remotely login to the linux lab using
    
    ssh -X username@machinename
    
    where machinename is the address of a machine in the linux lab.
  • I would actually recommend the same if you have a Linux machine or Mac, unless you want to make some more substantial use of it.
    Installing the why3 system can be a bit tricky, and remote login might be sufficient for answering the coursework.
• SPARK Ada reports that my post conditions fail, how do I find the reason for it?
  • You can debug your program by replacing your post condition by a condition which expresses part of it.
    
    • For instance if your post condition is
      
      if <cond> then <ifcase> else <elsecase>
      
      You can create two temporary conditions
      
      if <cond> then <ifcase>
      
      and
      
      if not(<cond>) then <elsecase>
      
      If you now replace the post condition by one of the two you can identify whether the problem has to do with the if case or the else case of your condition (or both).
      
    • Similarly you can break longer chains
      
      If .. then .. elsif .. then ... elsif ..
      
      into subconditions.
    • If your problem has the form
      
      A and B
      
      you can break it up for testing into
      
      A
      
      and
      
      B
      
      
    • If your problem has the form
      
      If <cond> then A and B
      
      you can break it up for testing into
      
      If <cond> then A
      
      and
      
      If <cond> then B
      
      
• How do I run SPARK Ada from the commandline?
  • See the end of basic Usage of Spark Ada