Re: Redefinition of Equality

[dgibson@cayman.cis.ohio-state.edu (david scott gibson)]

In article <DyKEBH.Gp3@world.std.com>,
Robert A Duff <bobduff@world.std.com> wrote:

>Well, the goal is to make sure that the compiler can *check* that the
>abstract value of an 'in' parameter is not modified.  And any time you
>want to check things at compile time, you have to put up with rules that
>are more pessimistic than they might be.  In this case, the compiler
>knows nothing of you "abstract" values.  The language therefore requires
>it to check that the concrete values are not modified.
>
>The alternative would be for 'in' mode to just be a comment in the code,
>and the compiler wouldn't check anything.  Then you could modify the
>concrete value while making sure the abstract value is not modified.
>But that would obviously be error prone.
>
>I don't see any way around this.

I don't think there is an easy solution.  In RESOLVE the behavior of
the operation would be formally specified.  The requirement that the
abstract value of an 'in' mode (RESOLVE's 'preserves' mode in this
case) parameter not change becomes a proof obligation.  I understand
why Ada takes the conservative approach.  However, this approach seems
to force unnecessary copying of objects and forces the programmer to
reason about the code at a less abstract level.

>Consider:
>
>    X: constant Integer := 1;
>    ...
>    Y: Integer := Read_Data_From_Input_File;
>    X := Y; -- Illegal!
>
>Should the above be legal?  After all, if the programmer ensures that Y
>is 1, then there's no harm done.

You wouldn't want to allow this, but what if X were an 'in' mode
formal parameter?  Then code similar to this would generate a proof
obligation that could not be satisfied.  As long as some form of
verification process is applied faithfully, allowing 'in' mode
parameters to be changed should not be a problem.

>Consider:
>
>    Do_Something("string literal");
>
>If Do_Something is allowed to modify the concrete value of its "in"-mode
>parameter, what is the compiler supposed to do with the result?

Literal values would require some special handling in an "all objects"
framework.  I think there are several different strategies that could
be used.  Upon elaboration of the unit containing the string literal
(and perhaps multiple references to it), a single object could be set
up with the literal as its value.  The above call could then be
implemented as a call passing in a String object, not a string value.
The string object could be manipulated, but Do_Something would be
required, as above, to return with the object's value unaltered.  I
doubt many current Ada compilers are likely to take this approach :-).

Dave
dgibson@cis.ohio-state.edu