Prev: Sockets package in SPARK (Was: Lost in translation (with SPARKuser rules))
Next: Ada compilers written in ... (was: Re: Ada noob here! Is Ada widely used?)
From: Yannick Duchêne (Hibou57) on 28 May 2010 05:04
Le Fri, 28 May 2010 10:14:56 +0200, Phil Thornley
<phil.jpthornley(a)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.
From: stefan-lucks on 28 May 2010 08:17
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! ------
From: Phil Thornley on 28 May 2010 07:50
On 28 May, 10:00, Yannick Duchêne (Hibou57) <yannick_duch...(a)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
From: Phil Thornley on 28 May 2010 11:13
On 28 May, 12:50, Phil Thornley <phil.jpthorn...(a)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
From: Yannick Duchêne (Hibou57) on 28 May 2010 18:41
Le Fri, 28 May 2010 13:50:51 +0200, Phil Thornley
<phil.jpthornley(a)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.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3
Prev: Sockets package in SPARK (Was: Lost in translation (with SPARKuser rules))
Next: Ada compilers written in ... (was: Re: Ada noob here! Is Ada widely used?)