Re: "Object" types vs. "Value" types

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

In article <4j4p79$ls1@dayuc.dayton.saic.com>,
John G. Volan  <John_Volan@ccmail.dayton.saic.com> wrote:

>On the contrary, copying of state does not necessarily imply _creating_
>a new object.  The target object might already exist, and have existed
>for a long time.  Maybe you're confusiong "copying" with "cloning".
> ...
>I don't see how any "objects" are either created or destroyed by
>scalar assignment.  A variable that once held one value winds up
>holding another value.  

Of course, no scalar constructors or destructors get called.  It's
just that I'd like to think about all variables in a uniform manner.
For more complex structures, it seems natural to think of variables as
handles for objects.  I believe it would be useful to think of all
variables in this same way.  With this way of thinking, an Integer
variable identifies an Integer object with some state, an integer
value.  (Ada's undefined initial representations for scalar types have
caused serious problems for me here.)  The notion of assignment from
one variable to another doesn't seem to fit well in this model, but
that's where I was coming from.  I think it is confusing to use := for
two conceptually different operations - value assignment as with
scalars, and copying (with object creation and destruction) for more
complex objects when augmented with Adjust.  Your point that limited
types are most appropriate for objects is right on target.

>Could you elaborate on why you think aliasing makes reasoning about
>a program harder?

Well, of course, the side effects that can result from aliasing make
code more difficult to understand and reason about than code without
aliasing.  From a formal reasoning point of view, verification is much
simpler when proof rules can include the implicit assumption that the
states of all objects not explicitly mentioned in a statement do not
change.  I believe that trying to formally specify program behavior in
the presence of aliasing is very difficult.  In order to reason about
systems which use components that allow aliasing (e.g., a polylithic
list), it may be necessary to consider complex interactions between
many components.  For arbitrarily large and complex systems, I believe
that this thwarts the possibility of rigorous reasoning about the
behavior of the system as a whole.  The key problem here is allowing
the ill effects of pointers to cross module abstraction boundaries.

>objects could swap locations.  Similarly, when an object is moved from
>one location into an already-vacant location, leaving behind it a newly
>vacant location, I suppose you could look at that as swapping an object
>and a vacuum.

In RESOLVE however, all objects are initialized to the specified
initial value of their type, thus there are no variables which
represent "vacant locations".  Swapping of two objects always results
in exchanging two objects whose states correspond to two (well
defined) abstract values.

>This sounds a lot like some of Henry Baker's work.

Perhaps the conservation of objects aspect, but RESOLVE is not a
functional language which seems to be the primary focus of Baker's
work as I understand it.

>Perhaps we're using different definitions of the word "abstraction".
>In software terms, I tend to use Booch's definition:

Yes, I think that's the case.  I certainly see how an Ada Integer
satisfies a reasonable definition of an abstraction.  I'm just pushing
the term a little farther beyond the implementation language level.

>I have often thought that much of the trickyness of pointers (e.g.,
>dangling references, garbage generation, etc.) could be avoided if
>pointers were replaced with a more sophisticated abstraction that was
>bi-directional.  In other words, any time some object A referenced
>some other object B, not only would A "know" about the reference,
>but B would know about it as well, and would effectively be 
>referencing A in turn.  Disconnecting the reference from A to B
>would also mean disconnecting the reference from B to A.  Destroying
>an object would automatically entail disconnecting it from every
>other associated object, thereby guaranteeing that no dangling
>references would be left behind -- essentially, all associated
>objects would be notified of its demise.
>
>I can see how this might make it easier to reason about program
>correctness than raw pointers.  (Is that the sort of thing your
>"Chain_Position" component accomplishes?  The name is compelling.) 
>Note, however, that this does not eliminate "aliasing" in any way, it
>just makes it safer.

RESOLVE components Chain_Position, Directed_Acyclic_Graph, and
Permutation (for cyclic structures) provide limited and safe aliasing.
My earlier implication that aliasing was completely prohibited in
RESOLVE was misleading.  These components do not really hide aliasing
from the client, they just ensure any aliasing can only have local
effects.  As a result, most of the problems that can result from
aliasing can be avoided.  For each instance of Chain_Position,
component (package) level state is maintained and shared by all
variables of the exported Position type.  Chain_Position's interface
is such that operations on Position variables (which simulate
pointers) cannot have any effect on similar operations in another
module even when a single instance of Chain_Position is involved.  (If
a Position value is explicitly passed to another module, then its
effects will be specified by the module interfaces.)  Proof rules for
Chain_Position operations are not going to be trivial, but should be
manageable due to the localization of effects.  A good description of
this component is in the Proceedings of the 10th Annual National
Conference on Ada Technology (1992, pp.  82-97).  Note that in this
paper and in the current RESOLVE/Ada83 catalog, Chain_Position and
Directed_Acyclic_Graph are called One_Way_Nilpotent and
N_Way_Nilpotent respectively.

>In the meantime,
>could you post a summary of the ideas behind this "RESOLVE" language?

The fundamental principle of RESOLVE, is that of modular reasoning.
With a RESOLVE component, it is possible to reason about the
correctness of an implementation by only examining the component's
specification, its implementation, and the specification of any
components used by the implementation.  To support generality for
reuse, RESOLVE components are highly parameterized (making heavy use
of generics in RESOLVE/Ada).  To support efficiency at the algorithmic
level, RESOLVE uses swapping instead of copying for most data
movement.  The pervasive use of swapping has a profound influence on
how components are typically designed and implemented.  To support
understandability as well as verifiability, RESOLVE integrates a
model-based specification sub-language and an implementation
sub-language into a single unified language.  Following the RESOLVE
discipline results in components which are readily composed with each
other with little of the "glue" required by many other disciplines.
Weakness of RESOLVE include the fact that it currently does not
address concurrency and it has not been demonstrated on many large
applications.  Also, the RESOLVE language does not have a compiler,
and hence one of the motivations for RESOLVE/Ada and RESOLVE/C++
disciplines.  

The most recent published description of RESOLVE is:

Murali Sitaraman and Bruce W. Weide, editors.  Special Feature: 
Component-Based Software Using RESOLVE, ACM SIGSOFT Software
Engineering Notes, 19(4):21-67, October 1994. 

A good paper discussing swapping is:

Douglas E. Harms and Bruce W. Weide.  Copying and Swapping:
Influences on the Design of Reusable Software Components,
IEEE Transactions on Software Engineering, 17(5): 424-435, May 1991.

More RESOLVE references can be found at:

http://www.cis.ohio-state.edu/hypertext/rsrg/RSRG.html

>Not _me_, other folks are trying to. :-)  Anyway, I was allowing for the
>possibility of someone arguing thus:
>
>"A stack is a kind of value with operations such as:

This doesn't sound quite right -- a "value" with operations.  I think
of behavior as part of the OO notion of object, but not of value.

>    function Push (The_Stack : in Stack.Value; New_Item : in Item)
>        return Stack.Value;
>        
>    function Pop (The_Stack : in Stack.Value) return Stack.Value;
>
>"When you push an item onto a stack value you generate a new stack value
>that is one item deeper than the old stack value, with the new item at
>the top and all the old items in the same sequence but one level deeper
>than they were before.  When you pop a stack, you generate a new stack
>value that is one item less deep than the old stack value, without the
>old top item, and with all remaining items in the same sequence but one
>level shallower than before.
> ...
>Somewhat an unorthodox view of stacks, I admit, and it might be hard
>to implement efficiently.  However, there's nothing theoretically unsound
>about this, and it would, among other things, allow arbitrary composing of
>stacks-of-stacks (without aliasing).

Actually, this looks very familiar.  I implemented some ADT's in ML
not long ago and due to the functional nature of ML they basically
looked like those in your example.  There were some serious questions
about the possibility of efficient implementations as you suggest.  I
suppose in the functional world, it is reasonable to consider anything
as a value.  I see your point, but I'd be surprised to hear of a good
reason to build software like this in Ada.  Thanks for your insights.

Dave
--
dgibson@cis.ohio-state.edu