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

[Richard D Riehle <laoXhai@ix.netcom.com>]

In article <37e994c0@news1.prserv.net>,
	"Matthew Heaney" <matthew_heaney@acm.org> wrote:

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

No, Matt.  I am not putting a constraint on the supplier.  Rather,
I am in favor of making it possible for the supplier to constrain
her/his own design to ensure behavior as intended.  Moreover, I
think the supplier should be able to explicitly state that behavior
to the client.  Even further, a designer of an abstract class should
be able to state, in a parameter list, that there is an expectation
that certain subprograms, using specified parameters, will not alter
the content of those parameters.  

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

As noted my Mr. Lundquist ( the Rosen trick) and others, the type 
system is not sufficient, by itself.  This is why the type system
is supported by rules for visibility and accessibility.  The supplier
would not be constrained from making changes in to an access parameter
in a subprogram.  Rather, such changes would be proscribed in a
subprogram including a mode of access constant.  

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

Agreed. That "whatever is necessary" should include the ability to 
declare the expectations for an abstraction.  The notion of constant
functions does not get in the way of a supplier.  Rather, it provides
a sense of security to her/his original intentions.

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

Of course, in Ada, there is no indication to the client of what a 
post-condition might be. A comment is not sufficient since later 
modification might override the comment.  Instead, if the original
designer declares that a function is constant, that is part of the
contract and every future modification to that constant requires 
adherence to that contract.  

The constraint is not on the original designer.  In fact, it is the
original designer who declares the constraint.  Rather, it is on the
future maintenance programmer.  

>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 confess a certain interest in the assertion mechanisms of Eiffel, 
but these mechanisms are not unique to Eiffel.  They are widely
accepted in much of the literature of computer science.  As of now,
I consider the Ada model more appropriate to safety-critical software
for a lot of reasons.  This is not the time to enumerate these.

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

Postconditions are implied in the very fact of writing a subprogram.
The problem is that they are not always clear to the client of a 
contract.  For well-known applications such as data structures (your
example of a Stack) we have a reasonable expectation of behavior. For
other applications, we have no such intuitive expectation.  

An assertion in the form of a comment can never be trusted.  One that
is checked by the compiler (or RTE) is more trusted.  As assertions
become more complex,

                  Require (X  >= Y or (Z /= w) and (Q > P)

they become unwieldy and uncheckable except through theorem provers.
We are not yet at the point in software science that we can 
consistently prove such things reliably.

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

This does fly in the opposite direction of those who believe that
postconditions should publicly state the expectations of a contract.

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

Internal behavior reflects some expectation of an external client.  
Can the client rely on the contract.  Maintenance of internal 
behavior should reflect the rules of that contract.  A change of 
internal behavior and state that should not be overridden
at the whim of some maintenance programmer who finds it possible to 
take advantage of some side-effect at the expense of those external
expectations, at the expense of the contract.

Richard Riehle
richard@adaworks.com
http://www.adaworks.com