From: stefan-lucks@see-the.signature
Subject: Re: SPARK again : for-loop vs single loop - a strange case
Date: Fri, 28 May 2010 14:17:50 +0200
Date: 2010-05-28T14:17:50+02:00 [thread overview]
Message-ID: <Pine.LNX.4.64.1005281258340.31198@medsec1.medien.uni-weimar.de> (raw)
In-Reply-To: <op.vderib0cxmjfy8@garhos>
[-- Attachment #1: Type: TEXT/PLAIN, Size: 633 bytes --]
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! ------
next prev parent reply other threads:[~2010-05-28 12:17 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 [this message]
2010-05-28 22:52 ` Yannick Duchêne (Hibou57)
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox