parameter passing

[davidg@oravax.UUCP (David Guaspari)]

Here's why I asked whether it would be reasonable to assume that
parameters of the same type are passed in the same way.  My problem is
reasoning about the values of out or inout parameters of composite
types after exceptional exit.

There are useful, simple cases in which we know how to write the
intended programs (in a natural way) and convince ourselves that
they're correct.

1. Example: Consider 

  procedure add_item(comp: in out composite_type, i: item_type)

part of whose specification is

  If i is an inappropriate item, then raise the exception
  INAPPROPRIATE_ITEM and leave comp unchanged.

If comp is passed by copy, then this part of the specification is
satisfied free of charge, so (at least as far as the given spec is
concerned) we can safely reason about add_item under the assumption
that comp is passed by reference.

2. Generalizing the example: 

What the example really shows is that it's possible to reason easily
about *invariant properties* of writable composite parameters -- i.e.,
about specifications like

  (*)  If some_exception is raised then (in the resulting exit state) 
       comp still satisfies some_property_it_satisfied_on_entry

It takes modest care to formulate "comp still satisfies ..." correctly. 

3. Generalizing too far: 

I'm involved in designing a specification language for Ada programs.
It permits you to say things like (*), but not to state any other
kinds properties of the value of comp upon exceptional exit.
Naturally, we want the class of permitted invariant properties to be
as general as possible (so long as we can still reason about them
easily).  Under Ada's rules, we're going too far if we permit the
invariant to be a joint property of two writable parameters, e.g. (for
the case in which composite_type is an array type (or, in the second
case, an array type with discrete components))

    if comp1 and comp2 are permutations of one another upon entry,
    then they are still permutations of one another upon exceptional
    exit

or

    the lexicographic ordering of comp1 and comp2 is the same on
    exceptional exit as it was on entry

For specifications like these, we can safely pretend that comp1 and
comp2 are passed by reference only if we are entitled to assume that
they're passed by the same mechanism.  

Hence my question.


David Guaspari
oravax!davidg@cu-arpa.cs.cornell.edu
davidg%oravax.uucp@cu-arpa.cs.cornell