Re: SPARK

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

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).

When (2) is there, it seems to forget about the previously proved  
hypothesis (1) or about hypotheses which make (1) provable.

Will have to better understand how this “thing” thinks.

-- 
There is even better than a pragma Assert: an --# assert