Need help understanding SPARK substitution rules

Need help understanding SPARK substitution rules

[Ben Hocking]

I have the following math.ads:
========
package Math is
   function IsPositive (InVal : in Integer) return Boolean;
   --# return (InVal > 0);
   function IsNegative (InVal : in Integer) return Boolean;
   --# return (InVal < 0);
   function AlwaysTrue (InVal : in Integer) return Boolean;
   --# return True;
end Math;
========
and math.adb:
========
package body Math is
   function IsPositive (InVal : in Integer) return Boolean is
   begin
      return (InVal > 0);
   end IsPositive;

   function IsNegative (InVal : in Integer) return Boolean is
   begin
      return (InVal < 0);
   end IsNegative;

   function AlwaysTrue (InVal : in Integer) return Boolean is
   begin
      --# 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 (not IsPositive(InVal) or not IsNegative(InVal));
   end AlwaysTrue;
end Math;
========
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).

However, this seems like a very fragile way of assuring code correctness, so it reeks from "code smell". What is a better way of achieving this?

Thanks,
-Ben

Re: Need help understanding SPARK substitution rules

[Phil Thornley]

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

Re: Need help understanding SPARK substitution rules

[Ben Hocking]

That solved the problem without the distaste.

Thanks, Phil.
-Ben