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

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

In article <7s9nd0$cbe@dfw-ixnews17.ix.netcom.com> , Richard D Riehle 
<LaoXhai@ix.netcom.com>  wrote:

> Ada does not support post-conditions.  I am not persuaded that a comment will
> have any effect on a client of a design.

Every operation has a precondition and a postcondition, irrespective of
whether of not it is expressed in the language proper.

For example:

  procedure Push
    (Item  : in     Item_Type;
     Stack : in out Stack_Type);
  --
  -- Precondition :
  --    not Is_Full (Stack)
  --
  -- Postcondition :
  --
  -- Get_Top (Stack) = Item
  -- Depth (Stack) = Depth (old Stack) + 1


If operations don't have postconditions, then what does invoking an
operation mean?


> We will have to agree to disagree on this.  It is a simple proposition.
> Permit a designer to designate an access parameter to be constant.  The client
> has a guarantee there will be no change to the incoming data.  I am not sure
> why this is so difficult.  We would be taking away nothing in flexibility and
> adding something in terms of the contract.

I think we're in violent agreement.

For non-private types, I think we can all agree that letting the caller know
there will be no state changes is A Good Idea.  Here it's easy to specify a
postcondition that means "no state change," because the state is a public
part of the object.

However, for private types, there is no such thing as "public state," so
there is obvious difficulty in specifying a postcondition that means "no
state change."


>>How would you even write a postcondition that says "internal state of object
>>hasn't changed"?  You're making a statement about internal behavior, in a
>>postcondition that describes external behavior.
>
> There are no postconditions in Ada, as mentioned earlier.

Disagree.  There are postconditions, it's just that they aren't expressible
in the language proper.


> Instead of a post- condition, we can guarantee the immutability of the data,
> in the specification of the subprogram, by making an access parameter
> constant.

I think we agree that for non-private types, this is a good idea.


>>(And remember, I'm only talking about internal state changes to limited
>>private, by-reference types.  Objects that are limited are always variables,
>>never constants.)
>
> I am actually not objecting to you notion regarding limited private,
> by-reference types.

Again, we seem to be in agreement.


> We are all agreed that the problem of modifying an access value can occur in
> Ada.  We simply do not agree that it is worth closing the loophole created by
> this feature.

I think we do agree that it is worth closing this loophole.

Matt
--
Help keep evolution in the science classroom and religion out: become a
member of the National Center for Science Education.

<http://www.natcenscied.org/>