Re: Making guarantees about record components

[Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org>]

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