@BOOK{liskov:abstr-and-spec,
  title =	"Abstraction and Specification in Program Development",
  author =	"Barbara Liskov and John Guttag",
  publisher =	"{MIT} Press",
  year =	1986,
  comment =	{Very readable book which presents a fairly informal
    	introduction to CLU and program development therein.
	Also includes an informal intro. to a subset of LARCH.
	Appendix contains (informal) specifications of common ADTs.

	Discusses the importance of abstraction (and decomposition)
	and emphasises both abstraction by parameterization and
	abstraction by specification.

	Classifies ADT operations into:
		primitive constructors
			     - return new ADT objects without
				taking any args of that type
		constructors - same, but can have args of the ADT type
		mutators     - modify ADT objects (mutable types only)
		observers    - take ADT objects and return other types).

	Notes on CLU:  	Supports procedural, data and iterator abstraction,
	and Ada-like generics (however, constrained generic ADTs can put
	the constraint on individual operations rather than the whole thing,
	see page 81).  Arrays can grow/shrink and are typically created
	empty, although a construct like \texttt{array[int]\$[3: 1,2,3]} can
	be used to create non-empty arrays with different bounds.
	Objects are heap allocated and garbage collected and can be mutable
	or immutable.  Composite object types are:-

				Mutable		Immutable
		Homogeneous	array		sequence
		Heterogeneous	record		struct
		Tagged union	variant		oneof

	For instance, `record' objects provide `set_<field>' operations
	that update the record, whereas `struct' objects provide
	`replace_<field>' operations that return a copy of the struct
	that differs in one element.  Strings are immutable and have
	a concatenation operation.

	Recommends that all ADT (including built-ins) follow the
	following conventions for `equal', `similar' and `copy'.
		equal - iff they are indistinguishable (for mutable
			objects, this means they must be the SAME object).
		similar - they contain similar values (ie. deep equal)
		copy - returns a `similar' value that does not share
			any components with the argument.

	Procedures can return multiple results and have informal pre/post
	conditions.  Functions are just procedures that return results.
	Declarations can appear anywhere (scope is to end of body) and
	can be combined with assignment: `x,y:int := div(3,4)' (where
	`div' returns two results).  Parameters are passed by `sharing'
	meaning that changes to mutable objects are visible to the caller.
	Infix, selection and array expressions etc. are just sugared
	procedure calls.  Procedures and iterators are first class objects.

	Pages 208-215 discuss more formal notation for CLU specifications.
	They introduce the following predicates for use in pre/post conds:

		x_{obj}		% stands for object bound to formal `x'
		x_{pre}		% value of object bound to formal `x'
				  when procedure was called.
		x_{post}	% value of object bound to formal `x'
				  when procedure returns.
		   Also, unqualified *argument* formal `x' == x_{pre}
		   and unqualified *result* formal `x' == x_{post}.
		   The _{obj} qualifier is *always* used on arguments
		   to the `new' and `modifies at most' predicates.

		modifies at most (<obj_list>)
		new(<obj>)
		returns		% procedure returns in normal way
				  (ie. does not abort, loop or signal)
		signals <name>	% procedure raises given exception
				  (which must be listed in proc. header)

	General form of a post-condition is:

		normally <post_pred>
		except  signals <except1> when <pre1> ensuring <post1>
			...
			signals <exceptN> when <preN> ensuring <postN>

	    which is equivalent to:
	    
		(returns | signals <except1> | ... | signals <exceptN>) &
		(returns => <post_pred> & ~(<pre1>|...|<preN>)) &
		(signals <except1> => (<pre1> & <post1>)) &
		  ...
		(signals <exceptN> => (<preN> & <postN>))
		
	This allows a nondeterministic choice of signals.
	Also, the `ensuring' clause is optional and defaults to TRUE.
	}
}