Re: Need help understanding SPARK substitution rules

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <84581b9d-040b-493b-a8af-ab3499001b5d@googlegroups.com>, 
benjaminhocking@gmail.com says...
> 
> I have the following math.ads:
[code snipped]
> The statement "check not (InVal > 0) -> InVal <= 0" is proven easily
> enough, but the next line ("check not IsPositive(InVal) -> InVal <=
> 0") is not, even though it's functionally equivalent. If I put the
> following line in math.rlu:
> ========
> math_ispositive: ispositive(inval) may_be_replaced_by (inval > 0)
> ========
> It now can prove it, and if I do the same thing with isnegative, the
> whole thing proves out (with the "return True" component being proven
> by ViCToR).
> 

What you need is for the Examiner to include the return expressions in 
the hypotheses - it does (now) do this, but only for VCs generated for 
code that follows the function call. (See Proof Manual Section 8.4.9 - 
bullet point 4)

So if you change your code to

   function AlwaysTrue (InVal : in Integer) return Boolean is
      Result : Boolean;
   begin
      Result := (not IsPositive(InVal) or not IsNegative(InVal));
      --# check not (InVal > 0) -> InVal <= 0;
      --# check not IsPositive(InVal) -> InVal <= 0;
      --# check not (InVal < 0) -> InVal >= 0;
      --# check not IsNegative(InVal) -> InVal >= 0;
      return Result;
   end AlwaysTrue;

then the VCs generated for the check annotations include hypotheses such 
as:
H7:    ispositive(inval) <-> (inval > 0) .

Now the only VC left unproven by the Simplifier is the last one (which 
you note is proved by Victor).

For those of us who (so far) find Victor (I loathe that casing they've 
adopted) not practicable for anything other than trivial code snippets, 
the one remaining VC can be proved by the rule:

boolean(1): not A or not B
              may_be_deduced_from
          [ A <-> X > 0,
            B <-> X < 0 ] .

which has the merit of being universally true and avoiding any "code 
smell".

Furthermore this rule can then be validated by proving the corresponding 
VC:

H1:  a <-> x > 0 .
H2:  b <-> x < 0 .
   ->
C1:  not a or not b .

(There are hints that this approach to validating rules will be 
described in the next version of the SPARK book).

Cheers,

Phil