Re: Using .rlu files in SPARK Ada

[Ben Hocking <benjaminhocking@gmail.com>]

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