A Train controller written in Ada-SPARK

• Uses Preconditions and Postconditions in order to create a safety critical system
• Compiles at SPARK gold level guaranteeing the absence of run time errors
• Has a console based GUI from where you can control the train, actions will not be accepted unless the preconditions are satisfied.

---

How to run the program

UNIX based system

• Execute main file from your terminal, with ./main.

Windows based system:

• Compile and run code in GNAT programming studio.

---

Controller Structure

• Program specification with preconditions and postconditions: trains.ads
• Program implementation with procedures and functions: trains.adb
• Main script: main file