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: 
 border1.nntp.dca3.giganews.com!backlog3.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin1!goblin.stu.neva.ru!eternal-september.org!feeder.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org>
Newsgroups: comp.lang.ada
Subject: Re: Making guarantees about record components
Date: Tue, 19 Nov 2013 15:57:22 -0700
Organization: Also freenews.netfront.net; news.tornevall.net
Message-ID: <l6gqci$lrk$1@dont-email.me>
References: <l6gbro$1oc$1@loke.gir.dk>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 19 Nov 2013 22:57:25 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="422f1844605d276c4d2d5781685aa881";
 logging-data="22388"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX19Mpb+qz9pgpfXxgeMgZYrhthvL2hk2TTc="
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
 rv:24.0) Gecko/20100101 Thunderbird/24.0
In-Reply-To: <l6gbro$1oc$1@loke.gir.dk>
Cancel-Lock: sha1:XZLn9mG4RHzVak1Cp4VuO8FHol4=
X-Original-Bytes: 1999
Xref: number.nntp.dca.giganews.com comp.lang.ada:183938
Date: 2013-11-19T15:57:22-07:00
List-Id: <comp.lang.ada>

On 11/19/2013 11:49 AM, J Kimball wrote:
>
> I'm trying to guarantee that two record component values map to the same
> value of another type.
>
> type A is (...);
> type C is (...);
>
> M : array (A) of C := (...);
>
> type R is record
>     A1 : A;
>     A2 : A;
> end record
>     with Dynamic_Predicate => (M (R.A1) = M (R.A2) );
>
> Is this the best solution we have as of Ada 2012?

If you really want to guarantee that the property always holds, this doesn't do 
that. Changes to components of variables of type R, and changes to M, may 
invalidate the predicate but not be detected until later. To really guarantee 
the property, you'd have to encapsulate M and all instances of R so that all 
such changes can be checked.

-- 
Jeff Carter
"There's no messiah here. There's a mess all right, but no messiah."
Monty Python's Life of Brian
84