Using .rlu files in SPARK Ada

Using .rlu files in SPARK Ada

[Ben Hocking]

I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine.

I've been unable to satisfy the following check statement:
   a2 := x3 - x1;
   b := y3 - y1;
   --# check b < a2 -> (b rem a2 = b);

It generates the following VC:
y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1

In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have:
small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1].

(Note that I originally had:
small_rem: x rem y = x may_be_deduced_from [x < y].

However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.)

Am I doing something incorrectly, or is there some limitation of SPARK here?

Re: Using .rlu files in SPARK Ada

[Phil Thornley]

In article <bbdd7647-8a13-41e1-9db7-b6842c22db0e@googlegroups.com>, 
benjaminhocking@gmail.com says...
> 
> I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine.
> 
> I've been unable to satisfy the following check statement:
>    a2 := x3 - x1;
>    b := y3 - y1;
>    --# check b < a2 -> (b rem a2 = b);
> 
> It generates the following VC:
> y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1
> 
> In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have:
> small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1].

To avoid any additional complications, I'll start by assuming that a2 
and b are guaranteed to be Positive (and there should really be 
something in the rule for that).

For a deduction rule to work, the formula that is deduced has to match 
the conclusion and the sideconditions have to match hypotheses (or be 
provable from the hypotheses).

This rule would work if the equality was the conclusion and
y3 - y1 < x3 - x1 were a hypothesis.

Since the conclusion is an implication, that is what the rule must be.

So you can either use:
small_rem: y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 
- x1) = (y3 - y1) may_be_deduced .

or change the code to:
   a2 := x3 - x1;
   b := y3 - y1;
   if b < a2 then
      --# check b rem a2 = b;
      null;
   end if;

(I have occasionally used null conditional statements to avoid complex 
implications.)

>
> (Note that I originally had:
> small_rem: x rem y = x may_be_deduced_from [x < y].
>
> However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.)
>
> Am I doing something incorrectly, or is there some limitation of SPARK here?

This never had a chance of working because rem is not an FDL operator 
(which is why the Examiner expands it out.)

However you also need to understand the use of wildcards in rules. This 
is covered in Section 7 of the Simplifier User Manual, but, briefly, 
anything in lower case in a rule formula has to match the text of the VC 
precisely (so the above rule would not work if you changed any of x1, 
x3, y1, y3 to something else).

Any name in a rule that starts with an upper-case character is a wild-
card (aka 'Prolog variable') that can be matched to any expression 
within a VC, so the ideal rule for your present code is probably:
small_rem: A < B -> A - A div B * B = A may_be_deduced .

or, to make sure it doesn't get used incorrectly anywhere else:
small_rem: A < B -> A - A div B * B = A may_be_deduced_from
           [A >= 0, B > 0,
            goal(checktype(A, integer)),
            goal(checktype(B, integer)) ] .
           
(and there's probably another for negative A and B as well).

Warning: all above expressions typed without any checking with SPARK 
tools.

Cheers,

Phil

Re: Using .rlu files in SPARK Ada

[Ben Hocking]

On Monday, August 13, 2012 11:46:04 AM UTC-4, Phil Thornley wrote:
> In article <bbdd7647-8a13-41e1-9db7-b6842c22db0e@googlegroups.com>, 
> 
> Ben says...
> 
> > 
> 
> > I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine.
> 
> > 
> 
> > I've been unable to satisfy the following check statement:
> 
> >    a2 := x3 - x1;
> 
> >    b := y3 - y1;
> 
> >    --# check b < a2 -> (b rem a2 = b);
> 
> > 
> 
> > It generates the following VC:
> 
> > y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1
> 
> > 
> 
> > In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have:
> 
> > small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1].
> 
> 
> 
> To avoid any additional complications, I'll start by assuming that a2 
> 
> and b are guaranteed to be Positive (and there should really be 
> 
> something in the rule for that).
> 
> 
> 
> For a deduction rule to work, the formula that is deduced has to match 
> 
> the conclusion and the sideconditions have to match hypotheses (or be 
> 
> provable from the hypotheses).
> 
> 
> 
> This rule would work if the equality was the conclusion and
> 
> y3 - y1 < x3 - x1 were a hypothesis.
> 
> 
> 
> Since the conclusion is an implication, that is what the rule must be.
> 
> 
> 
> So you can either use:
> 
> small_rem: y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 
> 
> - x1) = (y3 - y1) may_be_deduced .
> 
> 
> 
> or change the code to:
> 
>    a2 := x3 - x1;
> 
>    b := y3 - y1;
> 
>    if b < a2 then
> 
>       --# check b rem a2 = b;
> 
>       null;
> 
>    end if;
> 
> 
> 
> (I have occasionally used null conditional statements to avoid complex 
> 
> implications.)
> 
> 
> 
> >
> 
> > (Note that I originally had:
> 
> > small_rem: x rem y = x may_be_deduced_from [x < y].
> 
> >
> 
> > However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.)
> 
> >
> 
> > Am I doing something incorrectly, or is there some limitation of SPARK here?
> 
> 
> 
> This never had a chance of working because rem is not an FDL operator 
> 
> (which is why the Examiner expands it out.)
> 
> 
> 
> However you also need to understand the use of wildcards in rules. This 
> 
> is covered in Section 7 of the Simplifier User Manual, but, briefly, 
> 
> anything in lower case in a rule formula has to match the text of the VC 
> 
> precisely (so the above rule would not work if you changed any of x1, 
> 
> x3, y1, y3 to something else).
> 
> 
> 
> Any name in a rule that starts with an upper-case character is a wild-
> 
> card (aka 'Prolog variable') that can be matched to any expression 
> 
> within a VC, so the ideal rule for your present code is probably:
> 
> small_rem: A < B -> A - A div B * B = A may_be_deduced .
> 
> 
> 
> or, to make sure it doesn't get used incorrectly anywhere else:
> 
> small_rem: A < B -> A - A div B * B = A may_be_deduced_from
> 
>            [A >= 0, B > 0,
> 
>             goal(checktype(A, integer)),
> 
>             goal(checktype(B, integer)) ] .
> 
>            
> 
> (and there's probably another for negative A and B as well).
> 
> 
> 
> Warning: all above expressions typed without any checking with SPARK 
> 
> tools.
> 
> 
> 
> Cheers,
> 
> 
> 
> Phil

Thanks, Phil. That solved my problem.

Best regards,
-Ben