Saturate Angle

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.