This shows basic use of SPARK operators, statements and contracts. In the initial version, the postcondition of the function cannot be proved and a run-time check might fail. A precondition is required to fix both issues.
This shows basic use of SPARK modular types (the unsigned of C/C++) with bitwise operators, and a contract relating input and output values of a procedure. In the initial version, the postcondition cannot be proved because a xor operation is missing. And yes, 3 xor equal a swap!
This shows basic use of a protected object to communicate between two tasks. In the initial version, two tasks may access concurrently a global variable without adequate synchronization.
This shows basic use of the standard command line facilities to print a "hello, world" type of message on the standard output. In the initial version, the precondition of a call to a standard function may be violated. This must be fixed to prove the example.
This shows basic use of object orientation in SPARK, with an interface type being derived into a tagged type. In the initial version, the safety of behavioral subtyping (weakening of preconditions and strengthening of postconditions) between the parent interface and the derived type cannot be proved. In the proved version, behavioral subtyping ensures that a dispatching call to the procedure satisfies the precondition of the call, whatever the dynamic type of the object.
This shows basic use of generics in SPARK, with a generic function being instantiated for two scalar values, and a contract on the generic function. In the initial version, the postcondition of the instance cannot be proved, due to a user mistake on the instantiation.
This shows basic use of fixed-point types in SPARK (real types with a fixed precision contrary to floating-point types) and variables with memory-mapped addresses for sensors. In the initial version, the postcondition of a local function cannot be proved due to missing parentheses in an expression.
This shows basic use of arrays and strings in SPARK, with a rich postcondition quantifying over the content of strings, and a loop invariant stating the same property during loop iteration. In the initial version, the example cannot be proved due to a subtle off-by-one error.