comp.lang.ada
 help / color / mirror / Atom feed
From: "Constantin Porphyrogenete" <excubiteur@hotmail.com>
Subject: loop variant in SPARK ADA
Date: 19 Sep 2005 02:25:42 -0700
Date: 2005-09-19T02:25:42-07:00	[thread overview]
Message-ID: <1127121942.777976.45330@f14g2000cwb.googlegroups.com> (raw)

Couldn't find the newsgroup for SPARK.
Thought I'd try this one.

Read the book. It seems there is no
way to assert a loop variant to
help prove termination (I am thinking
of the Eiffel loop variant).

Is there any reason SPARK ADA doesn't
have this?




             reply	other threads:[~2005-09-19  9:25 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2005-09-19  9:25 Constantin Porphyrogenete [this message]
2005-09-19 13:23 ` loop variant in SPARK ADA Jacob Sparre Andersen
2005-09-19 15:40 ` Jeffrey Carter
2005-09-19 16:03   ` Georg Bauhaus
2005-09-19 22:22     ` Jeffrey Carter
2005-09-20  8:17       ` Georg Bauhaus
2005-09-20 17:15 ` Rod Chapman
2005-09-21  2:49   ` Constantin Porphyrogenete
2005-09-21 17:31     ` Jeffrey Carter
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox