SPARK Ada Examples for Getting Started (includes example similar to coursework)

Example for getting started with Question 1 of coursework 1

• Good example for getting started with Question 1 of coursework 1 is the clock example.
  • located in the git respository at
    ~/git/criticalhighintegritysystems/examplesForCoursework/conversion24hrClock12hrAMPMClock/
    Link to git repository
    
    • This directory contains several versions corresponding to different stages in answering your coursework question.
    • You can read the README.txt file located there for basic instructions.
    • It is best to study with a simple example, which forms a template for question 1 (a)
      • The example is
        ~/git/criticalhighintegritysystems/examplesForCoursework/conversion24hrClock12hrAMPMClock/withoutIO/vers01OnlyAdaWithIntegers/
        This example contains a simple program. It doesn't have (as all files in the subdirectory "withoutIO") a main file, so you can compile it but you don't obtain an executable file
        This allows you to focus on a simple package.
      • As always you should make a copy of that directory and work on that copy.
      • For the coursework 1 (a) you can comment out the definition of the function function, since we will create a function only later, once we have introduced a record type.
      • You cannot execute the code but check that it is syntactically correct by compiling it using
        gnatstudio → Build → Project → Build All
      • Now you can adapt it to a solution for Question 1 (a).
    • The second example includes an executable file and is a template for Question 1 (b).
      • The example is
        ~/git/criticalhighintegritysystems/examplesForCoursework/conversion24hrClock12hrAMPMClock/withIO/vers02OnlyAdaWithIOIntegersNoLibrary/
        
      • It contains a main.adb file, which is the executable file
      • This file you can compile (make sure main.adb is selected) by executing Build → Project → Build < current file >
        
      • You can run it as described in Basic Usage of gnatstudio by executing
        Build → Run → Custom
        Click on both "Run in executables directory" and "Run in an external terminal".
      • A terminal opens. In that opened terminal type in
        ./main
        ("main" is the executable file, and "./" makes sure that you execute the one in your current directory)
      • If nothing happens you may need to follow the instructions for setting up Spark Ada for Usage from File Manger and change preferences so that instead of "xterm -hold -e" you get the command "xterm -hold".
      • If everything was correct the main program of the clock example should start.
      • This example can be used as a template for answering question 1 (b)
    • For later parts of question 1, you can use further versions of the clock example as a template.

Further examples for getting started

• Examples using IO can be found in examplesIO
• Complete example with some guidance on how to use SPARK Ada (this is the example recommended in the Instructions for setting up SPARK Ada using file manager)
• Another example is
  sparkAdaCodeLecture/sect3c/example3c-14
  link to git repository
  This is an example which will give an error message when running flow analysis, so it demonstrates how SPRAK Ada reports error. You can then go through and modify it.
• Examples of critical systems can be found here