Making guarantees about record components

Making guarantees about record components

[J Kimball]

Hello

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?

Regards

Re: Making guarantees about record components

[Anh Vo]

On Tuesday, November 19, 2013 10:49:26 AM UTC-8, 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?
 
I am not sure if it is the best solution. However, it should work based on your requirements.

A. Vo

Re: Making guarantees about record components

[Jeffrey Carter]

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

Re: Making guarantees about record components

[Shark8]

At the very least M ought to be constant.

Re: Making guarantees about record components

[Dmitry A. Kazakov]

On Tue, 19 Nov 2013 15:38:37 -0800 (PST), Shark8 wrote:

> At the very least M ought to be constant.

Yes, that the problem with the concept. A true invariant need not and does
not hold within a method. It holds only outside it.

When simply thrown at the object representation in the form of an arbitrary
constraint it does not work beyond simple examples.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Making guarantees about record components

[Stephen Leake]

Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:

> 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.

The rules for when the Dynamic_Predicate is checked are in LRM 3.2.3
31/3. To me, that says any changes to an object of type R are checked,
but not changes to M. 

There is no value for M that satisfies this constraint for all possible
values of R, so this does not seem like a well-defined problem.

I think you need a private type hiding both R and M to enforce this
constraint.

-- 
-- Stephe

Re: Making guarantees about record components

[Jeffrey Carter]

On 11/20/2013 02:36 AM, Stephen Leake wrote:
>
> The rules for when the Dynamic_Predicate is checked are in LRM 3.2.3
> 31/3. To me, that says any changes to an object of type R are checked,
> but not changes to M.

See also Note 6 of that section, which says, "the predicate of a record subtype 
is not checked when a subcomponent is modified."

-- 
Jeff Carter
"Gentlemen, you can't fight in here. This is the War Room!"
Dr. Strangelove
30

Re: Making guarantees about record components

[tmoran]

> 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.

Re: Making guarantees about record components

[Stephen Leake]

Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:

> On 11/20/2013 02:36 AM, Stephen Leake wrote:
>>
>> The rules for when the Dynamic_Predicate is checked are in LRM 3.2.3
>> 31/3. To me, that says any changes to an object of type R are checked,
>> but not changes to M.
>
> See also Note 6 of that section, which says, "the predicate of a
> record subtype is not checked when a subcomponent is modified."

Ah, right. So

      R := (1, 2);

would be checked, but

      R.A1 := 3;

would not be checked.

-- 
-- Stephe

Re: Making guarantees about record components

[J Kimball]

On 11/19/2013 12:49 PM, J Kimball wrote:
> Hello
> 
> 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?
> 
> Regards
> 

Thanks for your inputs. I understand the rules for the dynamic_predicate
as Kazakov pointed out. This is what you'd expect certainly. I was more
curious to see what solutions you might propose. My solution uses a
variant. Subtypes of A become the mapping. Static predicates make this
even more powerful. Assuming you can put up with a discriminated record,
this solution doesnt show off the power of static predicates, but
demonstrates one solution not using private types or predicates and fits
my actual problem well.

type A is (...);

subtype E is A range ...;
subtype F is A range ...;

type C is (...);

type R (One : A) is record
   case One is
      when E =>
         E_Value : E;
      when F =>
         F_Value : F;
   end case;
end record;