Re: 'constant functions' and access constant params (was Re: Array of Variant Records Question...)

["Matthew Heaney" <matthew_heaney@acm.org>]

In article <7sas3p$bfa@dfw-ixnews3.ix.netcom.com> , Richard D Riehle 
<LaoXhai@ix.netcom.com>  wrote:

>>If operations don't have postconditions, then what does invoking an
>>operation mean?
>
> The question is, what does invoking an operation mean to the caller.

No.  The supplier defines what invoking an operation means.  The supplier
states this, explicitly or not, in the form of a postcondition.


> It is not easy to specify a post-condition.  The post-condition is implied,
> and becomes a client's best guess at your intention.

If this is the case, then clearly there is a problem.  There should be no
ambiguity about the meaning of an operation.


> If you could specify a post-condition for the function such as, (pseudocode),
>
>        Ensure(X before call = X after call);
>
> or even
>
>        Invariant(X always = X before call);
>
> the client would have assurance of the stability of X.

1) For non-private types, this is only an issue for access parameters.  We
both agree that we should be able to pass parameters as "access constant T",
in order to indicate to the client that no state change will occur.  (If you
don't need an access parameter, then just pass the parameter as in-mode.)

2) For private types, I say the "stability of X" is a meaningless statement.
A supplier's only obligation is to satisfy the postcondition, which has
nothing to say about internal state changes.  This is essentially where we
disagree (see below).


> This is not part of the Ada language, for good or bad.   Instead, we have the
> more conservative approach of range constraints, parameter modes, etc.  One of
> those parameter modes makes a parameter vulnerable to internal modification.

Yes, but this is only an issue for non-private types passed as an access
parameter.  An we agree that we would like to close this loophole by being
able to pass parameters as "access constant T".

For private types, the supplier is (or should be) free to make internal
modifications, to the extent that the postcondition is satisfied.  This is
where we disagree.


> Although there is no public state, a primitive operation with an access
> parameter can change the internal state of a parameter.  I think the guarantee
> of immutability is important for both private and non-private data.

Agree for non-private data.  Disagree for private data.


> Consider the following abstract class,
>
>       package Abstract_Level is
>           type Abstract_Declaration is abstract tagged private;
>           procedure X ( . . .) is abstract;
>           procedure Y ( . . .) is abstract;
>           function  F (A : access Abstract_Declaration) return some-type
>                                      is abstract;
>       private
>           type Abstract_Declaration is abstract tagged private;
>       end Abstract_Level;
>
> Now, anyone overriding function F can do so with implementing code that
> changes the internal state of the access parameter.

So what?  Suppose an internal state change is necessary in order to satisfy
the postcondition?  (This would still be true even if parameter A were
declared as "access constant Abstract_Declaration".)


> If, on the other hand, we were able to code the parameter so it would be a
> constant access,
>
>    function  F (A : access constant Abstract_Declaration) return some-type
>                                      is abstract;
>
> every overriding would be forced to leave the data in the parameter unchanged.

You seem to want to put a constraint on the supplier.  Why?

The type system is in place to prevent the client from breaking an
abstraction.  It is not in place to tie the supplier's hands behind his
back, so that he can be prevented from making internal state changes (to an
abstraction implemented as a private type).

The language should get out of the supplier's way, and let him do whatever
is necessary in order to implement an abstraction.

It doesn't make any difference to a client (of a private-type abstraction)
whether the data is changed or unchanged.  A client's only interest is in
whether the postcondition is satisfied, and state changes are not part of
the postcondition.



> Once again, what is our disagreement.  You just agreed with me on the very
> essence of my main point.  I am confused about where it is we don't agree.

We agree that the language should be amended to be able to pass parameters
as "access constant T" instead of just "access T", where T is any kind of
type.

We disagree about when an implementor of a private-type abstraction should
be allowed to make internal state changes.

I say the implementor of a private-type abstraction should be able to make
internal state changes, irrespective of the parameter mode.  Even if the
language were amended to pass access parameters as "access constant T", then
I still would want to be able to make internal state changes.

You say the implementor of a private-type abstraction should obey the
parameter modes, and only be able to change state when the parameter mode is
in-out mode or "access T" mode.  When the parameter mode is in-mode or
"access constant T" mode, then the supplier should not make internal state
changes.


I think the source of this disagreement stems from a couple of things:

1) Whether there are really postconditions in Ada (really, any language
other the Eiffel or Larch or ???).

I say yes, there are postconditions, even if they aren't officially
specified directly in the language.  You say no.


2) Whether an internal state change is part of a postcondition.

I say that for a private type, any statement about an "internal state
change" as part of a postcondition is meaningless, because a postcondition
only says what's true externally.

Even though you don't seem to recognize postconditions officially, you do
regard internal state changes as part of the defined, external behavior of a
private-type abstraction.

I don't regard internal state changes as part of the external behavior.


--
It is impossible to feel great confidence in a negative theory which has
always rested its main support on the weak points of its opponent.

Joseph Needham, "A Mechanistic Criticism of Vitalism"