From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: SPARK again : for-loop vs single loop - a strange case
Date: Sat, 29 May 2010 00:52:58 +0200
Date: 2010-05-29T00:52:58+02:00 [thread overview]
Message-ID: <op.vdftuknqxmjfy8@garhos> (raw)
In-Reply-To: Pine.LNX.4.64.1005281258340.31198@medsec1.medien.uni-weimar.de
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.
prev parent reply other threads:[~2010-05-28 22:52 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-27 19:36 SPARK again : for-loop vs single loop - a strange case Yannick Duchêne (Hibou57)
2010-05-27 21:50 ` Brian Drummond
2010-05-27 23:21 ` Yannick Duchêne (Hibou57)
2010-05-28 8:14 ` Phil Thornley
2010-05-28 9:00 ` Yannick Duchêne (Hibou57)
2010-05-28 11:50 ` Phil Thornley
2010-05-28 15:13 ` Phil Thornley
2010-05-28 22:46 ` Yannick Duchêne (Hibou57)
2010-05-28 22:41 ` Yannick Duchêne (Hibou57)
2010-05-28 9:04 ` Yannick Duchêne (Hibou57)
2010-05-28 12:17 ` stefan-lucks
2010-05-28 22:52 ` Yannick Duchêne (Hibou57) [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox