🚀 go-pugleaf

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)