Algorithms from ACSL by Example Sulfur edition. We use SPARK Discovery 2017 edition.
- level 0: everything is proved but overflow and range check (normal)
-level 0: everything is proved
- level 0: everything is proved
- level 0: everything is proved
- level 0: invariant preservation + postcondition not proved
- level 1: everything is proved
- level 0: invariant preservation + postcondition not proved
- level 1: everything is proved
- can be proved with SPARK GPL with a timeout of 30s on my machine. Can be proved easily with SPARK PRO 2017. Need investigation.
-level 0: Cannot prove Has_Sub_Range_In_Prefix function in loop invariant. -level 1: everything is proved
- no particular problem using axiomatic definition of Occ (see http:https://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_example/manual_proof.html#manual-proof-using-ghost-code)
- not using a Size parameter seems to make the proof easier
- functions Occ_Def and Occ are also proved
- easier than ACSL, no need to prove lemmas?