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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.