From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: tmoran@acm.org
Newsgroups: comp.lang.ada
Subject: Re: Making guarantees about record components
Date: Wed, 20 Nov 2013 20:58:09 +0000 (UTC)
Organization: Aioe.org NNTP Server
Message-ID: <l6j7p1$433$1@speranza.aioe.org>
References: <l6gqci$lrk$1@dont-email.me>
NNTP-Posting-Host: 1N/JdmS+b4dPz1bAuAPg+g.user.speranza.aioe.org
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
X-Newsreader: Tom's custom newsreader
Xref: news.eternal-september.org comp.lang.ada:17742
Date: 2013-11-20T20:58:09+00:00
List-Id: <comp.lang.ada>

> To really guarantee the property, you'd have to encapsulate M ...
  How many bugs have been caused by things like leaving out the first
line of
  Last := Last+1;
  Saved(Last) := New_Item;
(or misplacing the "++" in C code).
 The only way to ensure the abstraction of a data structure where Last
always points to the last item in Saved is by hiding it and
introducing an Append procedure.  For simple abstractions like this,
that's so heavy handed it's rarely done.  Predicates, as in the OP's
problem, are a very limited step toward eliminating this class of errors.