Re: SPARK

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sat, 15 May 2010 21:08:05 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Oh, something interesting:
>
>
>     procedure Limit
>       (X     : in out Integer;
>        Lower : in     Integer;
>        Upper : in     Integer)
>     --# pre    Lower < Upper;
>     --# post  ((X~ < Lower) -> (X = Lower)) and
>     --#       ((X~ > Upper) -> (X = Upper)) and
>     --#       (X in Lower .. Upper);
>
>     -- .....
>
>
>        Limit (Local_Data, Lowest, Highest);
>        --# assert Local_Data <= Highest;  -- (1)
>        Part := Local_Data - Lowest;
>        Whole := Highest - Lowest;
>        --# assert Part >= 0;              -- (2)
>        --# assert Local_Data <= Highest;  -- (3)
>
>     -- .....
>
>
> If (2) is removed, it can prove (1) and (3). If (2) is there, it fails  
> to prove (3), while nothing changes Local_Data in the path from (1) to  
> (3), and so (3) should be as much provable as (1).

If “assert” is replaced by “check” then it can prove (3) even if (2) is  
there. So that


      procedure Limit
        (X     : in out Integer;
         Lower : in     Integer;
         Upper : in     Integer)
      --# pre    Lower < Upper;
      --# post  ((X~ < Lower) -> (X = Lower)) and
      --#       ((X~ > Upper) -> (X = Upper)) and
      --#       (X in Lower .. Upper);

      -- .....


         Limit (Local_Data, Lowest, Highest);
         --# check Local_Data <= Highest;  -- (1)
         Part := Local_Data - Lowest;
         Whole := Highest - Lowest;
         --# check Part >= 0;              -- (2)
         --# check Local_Data <= Highest;  -- (3)

      -- .....

is OK.

So let's talk about “assert” vs “check”.

[Generation of VCs for SPARK Programs (2.2)] says:
> each assert or check statement in the code is located at a point in
> between two executable statements, in general, ie it is associated
> with a point on the arc of the flowchart of the subprogram which
> passes between the two statements it appears between. Each such
> assertion specifies a relation between program variables which must
> hold at that precise point, whenever execution reaches it. Assert
> statements generate a cut point on the flowchart of the subprogram,
> check statements do not.

What does “cut point” means precisely ? Is it related or similar to the  
unfortunately too much famous Prolog's cut ? This seems to be the next  
question to be answered, and a focus to care about for peoples learning  
SPARK.

Is that this “cut point” which makes Simplifier to forget about previous  
hypotheses when “assert” is used ? (if that's really similar to Prolog's  
cut, then indeed, it likely to make the prover loose memory)

About one of the most worthy thing with proving : what's the better way to  
give hints to the prover ? Is it “assert” or “check” ? This example  
suggest the best way is “check”. Is this example representative of most  
cases or a just a special case ?


--
There is even better than a pragma Assert: an --# assert (or a --#  
check.... question pending)