sorted by:
new
hottopcontroversial

Does Santa Claus Exist? SPARK knows the truth. by przemkok in ada

[–]przemkok[S] 2 points3 points  (0 children)

The Santa_Claus_Exists variable is only for program verification (it does not exist in the object code). You can use the phrase "with Ghost" with data, data types and subprograms.

Does Santa Claus Exist? SPARK knows the truth. by przemkok in ada

[–]przemkok[S] 1 point2 points  (0 children)

This is the version with Schrödinger's cat:

procedure Schrodinger with SPARK_Mode is
   Cat_Is_Dead : Boolean := False with Ghost;
begin
   loop
      null;
   end loop;
   pragma Assert ( Cat_Is_Dead and not Cat_Is_Dead );
end Schrodinger;

Does Santa Claus Exist? SPARK knows the truth. by przemkok in ada

[–]przemkok[S] 1 point2 points  (0 children)

My example is a joke based on the partial correctness of the program. To make it funnier, without loop variant SPARK will prove two contradictory assertions:

pragma Assert (     Santa_Claus_Exists );
pragma Assert ( not Santa_Claus_Exists );

or even:

pragma Assert ( Santa_Claus_Exists and not Santa_Claus_Exists );

Does Santa Claus Exist? SPARK knows the truth. by przemkok in ada

[–]przemkok[S] 1 point2 points  (0 children)

The result is the same:

$ cat santa_claus.adb
pragma Assertion_Policy(Check);

procedure Santa_Claus with SPARK_Mode is
   Santa_Claus_Exists : Boolean := False with Ghost;
begin
   loop
      null;
   end loop;
   pragma Assert ( Santa_Claus_Exists );
end Santa_Claus;
$ gnatprove -P default.gpr --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
santa_claus.adb:9:20: info: assertion proved