Compile_And_Prove_Demo/examples/absolute_value/example.yaml

name: Absolute Value
description: >
 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.