Re: SPARK

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

Another example, as much strange to me.


    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);
       Part := Local_Data - Lowest;
       Whole := Highest - Lowest;
       --# assert Part >= 0;
       --# assert Local_Data <= Highest;

    -- ....

The simplifier cannot prove “Local_Data <= Highest”, although the post  
condition of Limit states “X in Lower .. Upper” so that it should know  
“Local_Data in Lowest .. Highest” and then “Local_Data <= Highest”.

While perhaps I'm not using it the good way (as a beginner, this may be a  
possible case).

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