comp.lang.ada
 help / color / mirror / Atom feed
From: "Matthew Heaney" <matthew_heaney@acm.org>
Subject: Re: Safety of the Booch Ada 95 Components
Date: 1999/12/12
Date: 1999-12-12T00:00:00+00:00	[thread overview]
Message-ID: <3853f007_1@news1.prserv.net> (raw)
In-Reply-To: x7vu2lowfr2.fsf@pogner.demon.co.uk

In article <x7vu2lowfr2.fsf@pogner.demon.co.uk> , Simon Wright 
<simon@pogner.demon.co.uk>  wrote:

> The BCs equivalent for assignment is (no warranties, remember)
>
>   BB == BB' and (BA == BB'
>                  or an exception is raised)

That's exactly it.

Yes, this lacks "rollback semantics," but I'm perfectly happy with this
postcondition, as it's likely to be far more efficient than its stronger
alternative:

   HB == HB' and (HA == HB'
                  or an exception is raised and HA == HA')

I'd be willing to bet that most systems programmers would NOT be
satisfied with this postcondition, if they knew how inefficient it is
compared to the other.

Perhaps there is a middle position.  We could guarantee that if
assignment fails, then the target data structure is cleared, instead of
being left in some unknown state:

  HB == HB' and (HA == HB'
                 or an exception is raised and HA.Length == 0)


--
The political forces that try to eliminate evolution from science
classrooms impose a narrow, sectarian doctrine on our educational
systems. This imposition represents an affront not only to the
constitutional separation of church and state but also to the moral and
intellectual integrity embedded in that constitution.

<http://www.nabt.org/evolutionks.html>




  reply	other threads:[~1999-12-12  0:00 UTC|newest]

Thread overview: 29+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1999-12-10  0:00 Safety of the Booch Ada 95 Components Harry Erwin
1999-12-10  0:00 ` Matthew Heaney
1999-12-10  0:00   ` Hyman Rosen
1999-12-10  0:00     ` Matthew Heaney
1999-12-11  0:00       ` Harry Erwin
1999-12-12  0:00         ` Robert Dewar
1999-12-12  0:00           ` Harry Erwin
1999-12-13  0:00           ` Kent Paul Dolan
1999-12-13  0:00             ` Simon Wright
1999-12-13  0:00             ` Ted Dennison
1999-12-13  0:00             ` Robert I. Eachus
1999-12-13  0:00       ` Hyman Rosen
1999-12-13  0:00         ` Robert I. Eachus
1999-12-14  0:00           ` Simon Wright
1999-12-15  0:00             ` Harry Erwin
1999-12-15  0:00             ` Mats Weber
1999-12-17  0:00               ` Simon Wright
1999-12-14  0:00         ` Matthew Heaney
1999-12-10  0:00     ` Harry Erwin
1999-12-10  0:00   ` Harry Erwin
1999-12-12  0:00     ` Simon Wright
1999-12-12  0:00       ` Harry Erwin
1999-12-13  0:00         ` Simon Wright
1999-12-10  0:00 ` Simon Wright
1999-12-12  0:00   ` Simon Wright
1999-12-12  0:00     ` Matthew Heaney [this message]
1999-12-12  0:00   ` Harry Erwin
1999-12-13  0:00     ` Simon Wright
1999-12-13  0:00 ` Tucker Taft
replies disabled

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