From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: SPARK left/right shift.
Date: Tue, 21 Jul 2009 12:40:29 +0200
Date: 2009-07-21T12:40:29+02:00 [thread overview]
Message-ID: <4a659b1d$0$30227$9b4e6d93@newsspool1.arcor-online.net> (raw)
In-Reply-To: <6a8fc5de-7a2d-429c-81af-e1ac68e85b1f@t13g2000yqt.googlegroups.com>
xorque schrieb:
> I'm not currently writing anything that could be described
> as "high-integrity" but I try to use SPARK wherever possible
> as I do care deeply about software quality.
Can I second this? In writing a double buffer properly,
in particular when varying length characters need to be
handled, SPARK is really helpful, if only to sort out
and document the author's assumptions, omissions, and errors.
Same for a live topsorted structure that is waiting on
my shelf to be finished.
next prev parent reply other threads:[~2009-07-21 10:40 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-07-21 9:07 SPARK left/right shift xorque
2009-07-21 9:21 ` Rod Chapman
2009-07-21 9:31 ` Rod Chapman
2009-07-21 9:38 ` xorque
2009-07-21 9:54 ` Rod Chapman
2009-07-21 10:00 ` xorque
2009-07-21 10:40 ` Georg Bauhaus [this message]
2009-07-21 10:46 ` Jean-Pierre Rosen
2009-07-21 11:33 ` xorque
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox