SPARK again : for-loop vs single loop - a strange case
in [ADA]
|
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 27 May 2010 15:36 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.
From: Brian Drummond on 27 May 2010 17:50 On Thu, 27 May 2010 21:36:41 +0200, Yannick Duch�ne (Hibou57) <yannick_duchene(a)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
From: Yannick Duchêne (Hibou57) on 27 May 2010 19:21 Le Thu, 27 May 2010 23:50:06 +0200, Brian Drummond <brian_drummond(a)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.
From: Phil Thornley on 28 May 2010 04:14 On 27 May, 20:36, Yannick Duchêne (Hibou57) <yannick_duch...(a)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.
From: Yannick Duchêne (Hibou57) on 28 May 2010 05:00
Le Fri, 28 May 2010 10:14:56 +0200, Phil Thornley <phil.jpthornley(a)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. |