Re: SPARK

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

Currently, I'm reading Phil's documents, the ones in the directory  
Proof_Annotations and especially looking at exercises (yes, he created  
some) in part 5 to 9 and 12.

Part 5, exercise 4, turns to be something interesting to me, as it leads  
me to some questions about the way the simplifier is using hypothesis.

I would like to be more explicit. Here is the relevant part (slightly  
modified)


    ---------------------------------------------------------------------
    -- Exercise 5.4
    ---------------------------------------------------------------------
    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);
    is
    begin
       if X < Lower then
          X := Lower;
       elsif X > Upper then
          X := Upper;
       end if;
    end Limit;

    function Percent_Of_Range
      (Data    : Integer;
       Lowest  : Integer;
       Highest : Integer) return Percent_Type
    --# pre    (Lowest < Highest) and                        -- (1)
    --#        ((Highest - Lowest) <= Integer'Last) and      -- (2)
    --#        (((Highest - Lowest) * 100) <= Integer'Last); -- (3)
    --#
    is
       Local_Data : Integer;
       Part : Integer;
       Whole : Integer;
    begin
       Local_Data := Data;                                   -- (4)
       Limit (Local_Data, Lowest, Highest);                  -- (5)
       Part := Local_Data - Lowest;                          -- (6)
       Whole := Highest - Lowest;                            -- (7)
       return Percent_Type((Part * 100) / Whole);            -- (8)
    end Percent_Of_Range;


What's funny here, is about precondition line (2). If it is removed, the  
precondition become “(Lowest < Highest) and (((Highest - Lowest) * 100) <=  
Integer'Last)” and the simplifier fails to prove line (6) : it cannot  
prove the result will be lower than Integer'Last. I first though “(Highest  
- Lowest) * 100 <= Integer'Last” would be enough to also implies “Highest  
- Lowest < Integer'Last” ; it seems it is not. If you add precondition  
part (2), there is no more trouble with line (6).

Is this because of the way it is using hypotheses or is this because it  
miss some built-in rules to get all benefits from precondition part (3) ?

Now, there is still another unproved condition... at line (8), the  
simplifier cannot prove “((Local_Data - Lowest) * 100) / (Highest -  
Lowest) <= 100”. A first anecdote : funny to see it has expanded variables  
Part and Whole.

I wanted to solve in three steps and added the following between (6) and  
(7)


       --# assert Part <= Whole; -- (6.1)
       --# assert (Part * 100) <= (Whole * 100); -- (6.2)
       --# assert ((Part * 100) / Whole) <= ((Whole * 100) / Whole); --  
(6.3)


But the simplifier was not able to prove (6.1) nor (6.3) and was still not  
able to prove (8). About (6.2), and wanted to have a test, and added the  
following between (6.2) and (6.3):


       --# assert ((Part * 100) <= (Whole * 100)) ->
       --#        (((Part * 100) / Whole) <= ((Whole * 100) / Whole));


It was not able to prove it. Do I miss something or does it simply means  
the simplifier does not know about a rule which seems basic to me, that is  
(A <= B) -> ((A / C) <= (B / C)) ? ... which is still valid for integer  
arithmetic.

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