Wiki Agenda Contact Version française

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:


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.