Re: SPARK understand me very well... me neither

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

I have looked at it again, and cannot do better than stopping here:


    package Functions is
       function Multiply (A, B : Natural) return Natural;
       --# pre (A /= 0) -> (B <= (Integer'Last / A));
       --# return A * B; -- Implies commutativity on Multiply arguments
    end Functions;

    package body Functions is
       function Multiply (A, B : Natural) return Natural
       is
          Result : Natural;
       begin
          --# check (A = 0) -> ((A * B) = 0);
          --# check (A = 0) -> ((B * A) <= Integer'Last);
          --# check not (A = 0) -> (B <= (Integer'Last / A));
          --# check not (A = 0) -> ((B * A) <= (Integer'Last / A) * A);
          --# check not (A = 0) -> ((Integer'Last / A) * A <= Integer'Last);
          --# check not (A = 0) -> ((B * A) <= Integer'Last);
          -- Here is a gap which I cannot cross
          --# assert (A * B) <= Integer'Last;
          Result := A * B;
          return Result;
       end Multiply;
    end Functions;


Where I have marked “Here is a gap which I cannot cross”. A is either 0 or  
not 0, as (A = 0) -> ((B * A) <= Integer'Last) and
not (A = 0) -> ((B * A) <= Integer'Last) is proved, then (A * B) <=  
Integer'Last should be proved as well, as this finally turns into Any Case  
-> (A * B) <= Integer'Last. But no way to do, this only works with an  
if-then statement, and cannot do without it (and I do not want user rules  
here). I had a look at “SPARK/lib/checker/rules/LOGIC.RUL” to see what  
SPARK knowns from inborn, but just found these sole rules about “->” :


    /*** Other handy logical equivalences (DeMorgan, etc.) ***/

    logical(1):     not (A or B)     &   (not A) and (not B)     
are_interchangeable.
    logical(2):     not (A and B)    &   (not A) or (not B)      
are_interchangeable.
    logical(3):     A -> B           &   (not A) or B            
are_interchangeable.
    logical(4):     A <-> B          &   (A -> B) and (B -> A)   
are_interchangeable.
    logical(5):     A -> (B -> C)    may_be_replaced_by         (A and B)  
-> C.


And I would not want to turn X -> Y into (not X) or Y, as this would not  
create a nice example.

Note: you can see a concrete example of what I meant talking about P1 ->  
Pn when removing conditional statements. The four --#check prefixed with  
“not (A = 0) ->  ... ” match what was beneath the branch in the  
conditional statement where A /= 0. Do you see ?

Well, probably statements with logical branches, like if-then, or case,  
cannot be handle as easily using pure logical expressions. It had far less  
difficulties to fill the gap I point above when there was the if-then  
statement ; while without it, although with equivalent logical  
expressions, it cannot.