Computation of the trajectory of an object submitted to gravity
This example contains code from an embedded safety-critical software, which program computes the speed of a device submitted to gravitational acceleration and drag from the atmosphere around it.
This program was used as challenge example in the article Automating the Verification of Floating-Point Programs by Clément Fumex, Claude Marché, and Yannick Moy, published at VSTTE 2017 conference. This case study was initially provided by Florian Schanda from Altran, UK.
The Ada files contain multiple variants of the example in increasing order of difficulty:
- simple_trajectory_overflow.ads and simple_trajectory_overflow.adb Simple version of the computation, which only updates the speed by not the distance. Only absence of run-time errors (including overflows) is proved.
- simple_trajectory.ads and simple_trajectory.adb Simple version of the computation, which only updates the speed by not the distance. Both absence of run-time errors (including overflows) and safe bounds on the computed speed are proved.
- complex_trajectory_overflow.ads and complex_trajectory_overflow.adb More complex version of the computation, which updates both the speed and the distance. Only absence of run-time errors (including overflows) is proved, but this depends on the proof of safe bounds on the computed speed.
- complex_trajectory.ads and complex_trajectory.adb More complex version of the computation, which updates both the speed and the distance. Both absence of run-time errors (including overflows) and safe bounds on the computed speed and distance are expressed as properties, but the safe bounds on distance are not proved yet.
Authors: Clément Fumex / Yannick Moy
Topics: Floating-Point Computations
Tools: SPARK 2014
References: ProofInUse joint laboratory
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
The full code is in the ZIP archive above. Here is below the specification and the code for the simple trajectory.