pragma SPARK_Mode (On);
pragma Assertion_Policy (Pre => Check, Post => Check);