Absolute Value

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.