🚀 go-pugleaf

From grichard@skiff.cis.ohio-state.edu (Golden Richard):
> I'm all for reusable software components, but some reasonably formal system
> of specifying *exactly* what the components do and a verification method
> for providing better than "a 50-50 chance" of the components meeting specs
> are absolutely necessary.   

    Actually, one of the purposes of this group is to provide a forum
    in which manufacturers of substandard components can be identified
    (and given an opportunity to defend themselves).

    If such information is widely distributed throughout the component
    user community, then such companies can be subjected to the economic
    force of the market.  They will have to either improve their products
    or go out of business. 

    So if you have knowledge of a company which is marketing sloppy
    products (such as that so-far-unnamed company selling C components
    in New Jersey), please be quite specific; this will result in the 
    strengthening of the entire components market, to everyone's benefit.


    Bill Wolfe, wtwolfe@hubcap.clemson.edu
 

In article <60116@tut.cis.ohio-state.edu> Golden Richard <grichard@cis.ohio-state.edu> writes:
>I'm all for reusable software components, but some reasonably formal system
>of specifying *exactly* what the components do and a verification method
>for providing better than "a 50-50 chance" of the components meeting specs
>are absolutely necessary.   A major problem with using someone
>else's code in object form is that, barring a rigorous specification, it's 
>virtually impossible to ascertain *exactly* what a component does.

I've been reading Bertrand Meyer's book, and one of the ways Eiffel
enforces correctness is by specifying semantic assertions that must be
met by routines in a class.  Eiffel uses preconditions (require),
postconditions (ensure) and class invariants (invariant).
Preconditions and postconditions must only be met at the beginning and
end of a routine.  Class invariants must be met at all "stable" times
(between routine calls).  If you don't meet an assertion, an exception
is raised.  Also, hiers to a class must meet all the assertions of its
parent, so you can't change behavior by inheriting.  For example, the
ADT for a stack may look like (this is not Eiffel, just an ADT spec)


	TYPES			-- Syntax
		STACK[X]	-- Generic stack with type X
	FUNCTIONS		-- Syntax
		empty: STACK[X] -> BOOLEAN  --Accessor function. Stack on left
		new: -> STACK[X]	    --Creation function. Stack on right
		push: X x STACK[X] -> STACK[X] --Transformer function.
					       --Stack on both sides.
		pop: STACK[X] /-> STACK[X]      --Transformer. /-> denotes
						--partial function. I.e., 
						--function doesn't work for
						--all values (like stack
						--empty)
		top: STACK[X] /-> X	    --Accessor
	PRECONDITIONS		-- Semantics.  Clarifies partial functions.
		pre pop(s:STACK[X]) = (not empty(s))
		pre top(s:STACK[X]) = (not empty(s))
	AXIOMS			-- Semantics
		For all x:X, s:STACK[X]:
		empty(new())
		not empty(push(x,s))
		top(push(x,s))=x
		pop(push(x,s))=s
	
There is a lot of information there that specifies exactly how a stack
behaves.  You can model virtually all of this in Eiffel.

Here is an Eiffel implementation:

class STACK[T] 
export
	push, pop, top, empty, nb_elements, empty, full -- What clients can see
feature
	implementation: ARRAY[T];
	max_size: INTEGER;
	nb_elements: INTEGER;

	Create(n:Integer) is 
		-- Allocate stack for maximum of n elements
		-- (or for no elements if n < 0)
	do
		if n>0 then max_size := n end;
		implementation.Create(1, max_size)
	end; -- Create

	empty : BOOLEAN is
		-- Is stack empty?
	do
		Result := (nb_elements = 0)
	end; -- empty

	full : BOOLEAN is
		-- Is stack full?
	do
		Result ;= (nb_elements = max_size)
	end; -- full
	
	pop is
		-- Remove top element
	require		-- Precondition!
		not empty	-- i.e. nb_elements > 0
	do
		nb_elements := nb_elements - 1
	ensure		-- Postcondition!
		not full;
		nb_elements = old nb_elements - 1
	end; -- pop

	top : T is
		-- Top element
	require
		not empty -- i.e. nb_elements > 0
	do
		Result := implementation.entry(nb_elements)
	end; -- top

	push(x : T) is
		-- Add x on top
	require
		not full -- i.e. nb_elements<array_size in this representation
	do
		nb_elements := nb_elements + 1;
		implementation.enter(nb_elements, x)
	ensure
		not empty;
		top = x;
		nb_elements = old nb_elements + 1
	end; -- push

invariant	-- These always must satisfied at stable states.
	0 <= nb_elements; nb_elements <= max_size;
	empty = (nb_elements = 0)
end -- class STACK

The only AXIOM that is not ensured by this code is 

	pop(push(x,s)) = s

so you can see that enforcing correctness can be facilitated by the use
of assertions.
	Scott Simpson
	TRW Space and Defense Sector
	usc!trwarcadia!simpson  	(UUCP)
	trwarcadia!simpson@usc.edu	(Internet)

In article <60116@tut.cis.ohio-state.edu> Golden Richard <grichard@cis.ohio-state.edu> writes:
>Another (perhaps secondary) reason that I see for the current "low reuse"
>syndrome is the number of extremely sloppy components that are available.
>...[an example of buying object code] ... A major problem with using someone
>else's code in object form is that, barring a rigorous specification, it's 
>virtually impossible to ascertain *exactly* what a component does.   Having
>source is helpful, but who wants to poke through hundreds (thousands?) of
>pages of code "verifying" functionality?

I've had similar experiences with C library functions packaged with a
compiler, with 3rd party code that uses 'slightly' variant library
functions, and some OOP systems where the interface is formally spelled
out but the rest kept elsewhere - in all three cases, I've either needed
to hunt down the real source or waste a great deal of time probing a
black box.

In this day and age, few programmers would even poke through the lines
they wrote themselves without a symbolic debugger and if source is included,
all it takes is a single re-compile to create the step-able version.

And speaking of reuse, and this problem of source-code secrets, how does
this sit with the misplaced metaphor of software-as-literature with respect
to copyrights? (If I quote Tolstoy's first edition, and the passage is
stated contrarily in the fifth, do I still owe royalties? :-).
-- 
     Gary Murphy - Cognos Incorporated - (613) 738-1338 x5537    
  3755 Riverside Dr - P.O. Box 9707 - Ottawa Ont - CANADA K1G 3N3
          e-mail: decvax!utzoo!dciem!nrcaer!cognos!garym         
  Cosmic Irreversibility: 1 pot T -> 1 pot P, 1 pot P /-> 1 pot T

Being real process-oriented lately, I'd like to put this reuse discussion in
a broader setting.  Many assertions have been made about the possibilities
and issues of reuse, each based on unstated or only partially stated
assumptions about the process and setting of the supposed act of reuse.  In
fact, there can be many such settings, each implying different constraints
and characteristics of the components, the collection of them, and the
"reuser".  For example,

    The personal toolkit: an experienced machanic collects high-quality
    tools, assumes responsibility for them, and takes them with him/her.
    Having created a module to solve a problem, an experienced software
    engineer might well generalize the solution a bit, polish the
    implementation and the interface description, and drop it in the kit.

    The corporate resource: rather than continually reinventing solutions to
    recurring problems, the company creates a library and supporting staff
    to capture the solutions and make them available to new projects.  Note
    that there's likely some domain leverage here; the company's projects
    will often cover a lot of the same ground.

    The commercial product: this is what seems to have been the assumption
    behind most of the discussions so far.  Even here, there are many
    possible relationships among the component and library creators,
    sellers, and buyers, and probably many possible types of "component"
    (how about selling detailed designs or generic sources like MacApp?)

In all these settings, I think that the major problems are organizational,
psychological, and institutional -- meeting the differing goals of the
various folks involved.  It'll probably take some "process prototyping" to
work these out.  The technical problems that arise will be solved as part of
all this (and some technical issues will turn out to be non-problems).

What I'd like to see is some reuse success and horror stories along this
line: what was the setting and process, how did it work out, what problems
arose and how were they solved (if they were)?


--
Don Dwiggins				"Solvitur Ambulando"
Ashton-Tate, Inc.
dwiggins@ashtate.uucp