SPARK again : for-loop vs single loop - a strange case

SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Hi all,

This will require some further investigation on my own side, however, I  
would like to open a topic about it, if ever someone wants to share about  
the same matter.

I was proving something built around a for-loop. Every thing was going,  
when I've meet a trouble and decided to switch to a classic loop and an  
exit statement and a local variable.

There was a Check clause in the for-loop, which was looking like this:

    for L in T range 1 .. N loop
       ...
       --# assert ...;
       ...
       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
       ...
    end loop;


This Check clause was proved by the Simplifier without any trouble.

I then switch to a class loop, looking like this:


    L := 1;

    loop
       ...
       --# assert ...;
       ...
       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
       exit when L = Length;
       L := L + 1;
       ...
    end loop;

Then, the Simplifier was not able anymore to prove this Check. I don't  
understand, as this Check should only depends on a basic rule, a rule by  
definition. So why the same rule is not applied when I use a classic loop  
instead of a for-loop ?

Does SPARK changes its strategy depending on the structure of the  
surrounding source so that it may or may not found a match to a rule  
depending on this context ?

I've checked multiple times, this does not seems to be an error, it do the  
same each time I switch from one to the other.

Re: SPARK again : for-loop vs single loop - a strange case

[Brian Drummond]

On Thu, 27 May 2010 21:36:41 +0200, Yannick Duch�ne (Hibou57)
<yannick_duchene@yahoo.fr> wrote:

>Hi all,
>
>This will require some further investigation on my own side, however, I  
>would like to open a topic about it, if ever someone wants to share about  
>the same matter.
>
>I was proving something built around a for-loop. Every thing was going,  
>when I've meet a trouble and decided to switch to a classic loop and an  
>exit statement and a local variable.
>
>There was a Check clause in the for-loop, which was looking like this:
>
>    for L in T range 1 .. N loop
>       ...
>       --# assert ...;
>       ...
>       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>       ...
>    end loop;
>
>
>This Check clause was proved by the Simplifier without any trouble.
>
>I then switch to a class loop, looking like this:
>
>
>    L := 1;
>
>    loop
>       ...
>       --# assert ...;
>       ...
>       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>       exit when L = Length;
>       L := L + 1;
>       ...
>    end loop;
>
>Then, the Simplifier was not able anymore to prove this Check. I don't  
>understand, as this Check should only depends on a basic rule, a rule by  
>definition. So why the same rule is not applied when I use a classic loop  
>instead of a for-loop ?

Is it relevant here that the range of L is known in the first loop, and
can (presumably) be shown to be less than T'Size?

Perhaps L in the second example can be declared of a subtype with
appropriate range? (If it already is, that wasn't shown in the posted
code)

- Brian

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Thu, 27 May 2010 23:50:06 +0200, Brian Drummond  
<brian_drummond@btconnect.com> a écrit:
Hi Brian,

> Is it relevant here that the range of L is known in the first loop, and
> can (presumably) be shown to be less than T'Size?
>
> Perhaps L in the second example can be declared of a subtype with
> appropriate range? (If it already is, that wasn't shown in the posted
> code)
Yes, sorry, I forget it. In the simple loop case, L is of the same type,  
that is, it is declared as of type T and T'First is equal to 1. So the  
declaration of L in the for-loop and the declaration of L with the simple  
loop, are the same. N is obviously of type T too.

What puzzles me, is that the expression in the Check clause, does not  
depend on any context, it is purely mathematical, thus it should be as  
provable with the simple loop as it is with the for-loop.

I've just done a test a few seconds ago. If I copy the same Check clause  
between the “L := 1;” statement and the begin of the loop, that is:


    L := 1;

    --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);

    loop
       ...
       --# assert ...;
       ...
       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
       exit when L = Length;
       L := L + 1;
       ...
    end loop;

then the first occurrence of the Check, at the first location, is proved  
right away by the simplifier, and the second occurrence, is still not  
proved.

Really funny, as the expression does not depends on any context and all  
numbers/expression which appears in, are Universal_Integer [ARM 2005 Annex  
K (175)], so there should be no matter about any range of any kind. Note:  
T'Last is small, it is actually 8.

Will try some others things later. I believe this is an interesting topic  
(unless I did a gentle clumsy thing which I have not already figured).

Have a nice day/night.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK again : for-loop vs single loop - a strange case

[Phil Thornley]

On 27 May, 20:36, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
[...]
> There was a Check clause in the for-loop, which was looking like this:
>
>     for L in T range 1 .. N loop
>        ...
>        --# assert ...;
>        ...
>        --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>        ...
>     end loop;
>
> This Check clause was proved by the Simplifier without any trouble.
>
> I then switch to a class loop, looking like this:
>
>     L := 1;
>
>     loop
>        ...
>        --# assert ...;
>        ...
>        --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>        exit when L = Length;
>        L := L + 1;
>        ...
>     end loop;
>
> Then, the Simplifier was not able anymore to prove this Check. I don't  
> understand, as this Check should only depends on a basic rule, a rule by  
> definition. So why the same rule is not applied when I use a classic loop  
> instead of a for-loop ?
>
> Does SPARK changes its strategy depending on the structure of the  
> surrounding source so that it may or may not found a match to a rule  
> depending on this context ?

It is difficult to be specific about non-SPARKable code*, but one
difference at the check will be that the upper bound on L has been
lost.

You can get it back by adding L <= Length to the assertion.  [You
might also need to change the test to
exit when L >= Length;]

It is put in there aotomatically for a 'for' loop but not for a simple
loop.

Cheers,

Phil

* If the code is too big to put in a message then you can send it by
email to the address on the proof tutorials and I'll be happy to have
a look at it.

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 10:14:56 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> You can get it back by adding L <= Length to the assertion.  [You
> might also need to change the test to
> exit when L >= Length;]
>
> It is put in there aotomatically for a 'for' loop but not for a simple
> loop.
You're wonderful Phil! This was something near to that: I've added L <=  
Length, it was not OK, so I though if the upper bound hypothesis was lost,  
so as well was probably the one of the lower bound. So I've added L >= 1,  
then figured that the Checked expression was not verified for L lower than  
zero, so thought if one hypothesis was required, this was this only one,  
the one for the lower bound. So I removed the L <= Length and left L >= 1  
only, which was shown to be enough.

Without you, I would not have been able to guess the trouble was there, as  
to me, it was obvious L >= 1, as the type of L, which is really  
Length_Type, has Length_Type'First = 1.

This is still strange in some way, as if I do L >= Length_Type'First, it  
works.

So the Assert clause even drops implicit hypotheses about numeric type  
bounds ? I was thinking this ones were preserved even after an Assert  
clause.

I was pretty sure Assert was still preserving somethings, as I feel I  
remember I have read something suggesting that in one of the Praxis's  
documentation and in yours as well (do not remember which PDF file, and  
there many to check).

> * If the code is too big to put in a message then you can send it by
> email to the address on the proof tutorials and I'll be happy to have
> a look at it.
Not too big, this was just that as I was afraid my style with SPARK may  
not be good enough to be posted here. I have lot of lines of SPARK proofs  
for few lines of Ada text, which may seems silly to someones... also that  
I like to have explicit things, because it is more easy to understand and  
to track.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK again : for-loop vs single loop - a strange case

[Phil Thornley]

On 28 May, 10:00, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> [...] So I removed the L <= Length and left L >= 1  
> only, which was shown to be enough.
>
> Without you, I would not have been able to guess the trouble was there, as  
> to me, it was obvious L >= 1, as the type of L, which is really  
> Length_Type, has Length_Type'First = 1.
>
> This is still strange in some way, as if I do L >= Length_Type'First, it  
> works.
>
> So the Assert clause even drops implicit hypotheses about numeric type  
> bounds ? I was thinking this ones were preserved even after an Assert  
> clause.
>
> I was pretty sure Assert was still preserving somethings, as I feel I  
> remember I have read something suggesting that in one of the Praxis's  
> documentation and in yours as well (do not remember which PDF file, and  
> there many to check).

This thread persuaded me to finally check precisely what the Examiner
generates for local variables (I have always just assumed that it
doesn't do anything - looking back through the release notes, this
changed in Release 7.2).

The statement about this is in GenRTCs section 4.5.2.1; hypotheses are
generated that local variables are in-type if various conditions are
met that ensure that no out-of-type value can be assigned in the
procedure (no 'significant' data flow errors, no read from external
variables and no use of Unchecked_Conversion).

So the fact that adding L >= Length_Type'First allows the Simplifier
to prove the check suggests that you are not getting these hypotheses
- possibly for one of the above reasons.

If you should be getting these hypotheses then post (or email) the
complete SPARKable code.

Cheers,

Phil

Re: SPARK again : for-loop vs single loop - a strange case

[Phil Thornley]

On 28 May, 12:50, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> This thread persuaded me to finally check precisely what the Examiner
> generates for local variables (I have always just assumed that it
> doesn't do anything - looking back through the release notes, this
> changed in Release 7.2).
>
> The statement about this is in GenRTCs section 4.5.2.1; hypotheses are
> generated that local variables are in-type if various conditions are
> met that ensure that no out-of-type value can be assigned in the
> procedure (no 'significant' data flow errors, no read from external
> variables and no use of Unchecked_Conversion).

I seem to have reproduced the same problem as Yannick.

Here is the code:

   subtype Index is Integer range 1 .. 10;
   type Arr is array(Index) of Integer;

   procedure Zero_Part (A : in out Arr;
                        U : in     Index)
   --# derives A from *, U;
   is
      I : Index;
   begin
      I := 1;
      loop
         A(I) := 0;
         exit when I >= U;
         I := I + 1;
      end loop;
   end Zero_Part;

As I understand the documentation the default assertion should include
hypotheses that I is in-type, but when simplified there are two
conclusions left for the A(I) := 0; assignment:
C1:    i >= 1 .
C2:    i <= 10 .

If I add the assertion:
--# assert I in Index;
then these conclusions are proved by the Simplifier.

So either my understanding of how the Examiner generates hypotheses is
wrong or the Examiner is wrong.

Cheers,

Phil

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 17:13:57 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> As I understand the documentation the default assertion should include
> hypotheses that I is in-type, but when simplified there are two
> conclusions left for the A(I) := 0; assignment:
> C1:    i >= 1 .
> C2:    i <= 10 .
That's it.

> So either my understanding of how the Examiner generates hypotheses is
> wrong or the Examiner is wrong.
I would say the examiner is wrong, as 4.2 states it should really do as  
yourself expected.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 13:50:51 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> So the fact that adding L >= Length_Type'First allows the Simplifier
> to prove the check suggests that you are not getting these hypotheses
> - possibly for one of the above reasons.
OK, with the for-loop, L cannot goes outside of the range expression, so  
the Examiner can always assume these hypotheses exist. However, there is  
still the Length_Type and associated VC for RTC, which can turn into  
hypotheses. I would understand I may had a trouble with a VC associated to  
a RTC, I can't understand this one.

You suggested to look Generation of RTC, section 4.5.2.1.

It says:
> The default assertion states the subprogram’s precondition
> is satisfied
OK.

Then
> In the case of for loops, the invariant also states that theloop counter  
> is in its subtype.
OK.

I could not see something about local variables here indeed.

Something about it is said in 4.2:
> Additionally, the Examiner exploits the benefit of data
> flow analysis by assuming that a local variable, anywhereit is  
> referenced in an expression, must be validly in type.
providing there is no flow error, as explained later in 4.2

There was no flow error, so the Length_Type range should be enough as an  
hypothesis, and it should be there (and that was my assumption, that is  
why I did not understood what's happened).


> If you should be getting these hypotheses then post (or email) the
> complete SPARKable code.
Will see. I will try somethings else before.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 10:14:56 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> [...]

P.S. Just to tell more, I switched from a for-loop to a classic-loop, so  
as to be able to prove something after the loop, and this was not possible  
with a for-loop, as L is not anymore in the scope after the loop.

I feel classic-loop are probably more handy with proof, due to that it  
leaves some termination states accessible after the loop, and these are  
most likely needed hypothesis to prove many things after a loop.

Or may be I'm wrong ? Do you know a case where a for-loop is better than a  
classic-loop with proofs ?

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.

Re: SPARK again : for-loop vs single loop - a strange case

[stefan-lucks]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 633 bytes --]

On Fri, 28 May 2010, Yannick Duch�ne (Hibou57) wrote:

> Or may be I'm wrong ? Do you know a case where a for-loop is better than a
> classic-loop with proofs ?

A for-loop terminates always. 

A classical loop may run forever. One would prove termination by loop 
variants, but SPARK doesn't support loop variants. (I am sure you know 
that.)

I would consider this a reason to prefer for-loops over classical loops. 

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: SPARK again : for-loop vs single loop - a strange case

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 14:17:50 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> A for-loop terminates always.
>
> A classical loop may run forever. One would prove termination by loop
> variants, but SPARK doesn't support loop variants. (I am sure you know
> that.)
Right.

> I would consider this a reason to prefer for-loops over classical loops.
As much as possible, which may be not always.

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.