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 18:46
Le Fri, 28 May 2010 17:13:57 +0200, Phil Thornley
<phil.jpthornley(a)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.
From: Yannick Duchêne (Hibou57) on 28 May 2010 18:52
Le Fri, 28 May 2010 14:17:50 +0200, <stefan-lucks(a)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.
First  |  Prev  | 
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?)