$6.4 FORMALIZING THE SPECIFICATION 131 The TYPES paragraph simply lists the types introduced in the specification.Here: TYPES ·STACK[G Our specification is about a single abstract data type STACK,describing stacks of objects of an arbitrary type G. Genericity See"Genericity”, In STACK [G],G denotes an arbitrary,unspecified type.G is called a formal generic page 96. parameter ofthe abstract data type STACK,and STACK itself is said to be a generic ADT. The mechanism permitting such parameterized specifications is known as genericity;we already encountered a similar concept in our review of package constructs. It is possible to write ADT specifications without genericity,but at the price of unjustified repetition.Why have separate specifications for the types "stack of bank accounts","stack of integers"and so on?These specifications would be identical except where they explicitly refer to the type of the stack elements-bank accounts or integers. Writing them,and then performing the type substitutions manually,would be tedious. Reusability is desirable for specifications too-not just programs!Thanks to genericity, we can make the type parameterization explicit by choosing some arbitrary name,here G, to represent the variable type of stack elements. As a result,an ADT such as STACK is not quite a type,but rather a type pattern;to obtain a directly usable stack type,you must obtain some element type,for example 4CCOUNT,and provide it as actual generic parameter corresponding to the formal parameter G.So although STACK is by itself just a type pattern,the notation STACK [ACCOUNT] is a fully defined type.Such a type,obtained by providing actual generic parameters to a generic type,is said to be generically derived. The notions just seen are applicable recursively:every type should,at least in principle,have an ADT specification,so you may view ACCOUNT as being itself an abstract data type;also,a type that you use as actual generic parameter to STACK(to produce a generically derived type)may itself be generically derived,so it is perfectly all right to use STACK [STACK [ACCOUNT]] specifying a certain abstract data type:the instances of that type are stacks,whose elements are themselves stacks;the elements of these latter stacks are bank accounts. As this example shows,the preceding definition of "instance"needs some qualification.Strictly speaking,a particular stack is an instance not of STACK(which,as noted,is a type pattern rather than a type)but of some type generically derived from STACK,for example ST4CK [ACCOUNT].It is convenient,however,to continue talking
§6.4 FORMALIZING THE SPECIFICATION 131 The TYPES paragraph simply lists the types introduced in the specification. Here: Our specification is about a single abstract data type STACK, describing stacks of objects of an arbitrary type G. Genericity In STACK [G], G denotes an arbitrary, unspecified type. G is called a formal generic parameter of the abstract data type STACK, and STACK itself is said to be a generic ADT. The mechanism permitting such parameterized specifications is known as genericity; we already encountered a similar concept in our review of package constructs. It is possible to write ADT specifications without genericity, but at the price of unjustified repetition. Why have separate specifications for the types “stack of bank accounts”, “stack of integers” and so on? These specifications would be identical except where they explicitly refer to the type of the stack elements — bank accounts or integers. Writing them, and then performing the type substitutions manually, would be tedious. Reusability is desirable for specifications too — not just programs! Thanks to genericity, we can make the type parameterization explicit by choosing some arbitrary name, here G, to represent the variable type of stack elements. As a result, an ADT such as STACK is not quite a type, but rather a type pattern; to obtain a directly usable stack type, you must obtain some element type, for example ACCOUNT, and provide it as actual generic parameter corresponding to the formal parameter G. So although STACK is by itself just a type pattern, the notation STACK [ACCOUNT] is a fully defined type. Such a type, obtained by providing actual generic parameters to a generic type, is said to be generically derived. The notions just seen are applicable recursively: every type should, at least in principle, have an ADT specification, so you may view ACCOUNT as being itself an abstract data type; also, a type that you use as actual generic parameter to STACK (to produce a generically derived type) may itself be generically derived, so it is perfectly all right to use STACK [STACK [ACCOUNT]] specifying a certain abstract data type: the instances of that type are stacks, whose elements are themselves stacks; the elements of these latter stacks are bank accounts. As this example shows, the preceding definition of “instance” needs some qualification. Strictly speaking, a particular stack is an instance not of STACK (which, as noted, is a type pattern rather than a type) but of some type generically derived from STACK, for example STACK [ACCOUNT]. It is convenient, however, to continue talking TYPES • STACK [G] See “Genericity”, page 96
132 ABSTRACT DATA TYPES $6.4 about instances of STACK and similar type patterns,with the understanding that this actually means instances of their generic derivations. Similarly,it is not quite accurate to talk about STACK being an ADT:the correct term is "ADT pattern".For simplicity,this discussion will continue omitting the word "pattern"when there is no risk of confusion. The distinction will carry over to object-oriented design and programming,but there we will need to keep two separate terms: .The basic notion will be the class;a class may have generic parameters. .Describing actual datarequires types.A non-generic class is also a type,but a generic class is only a type pattern.To obtain an actual type from a generic class,we will need to provide actual generic parameters,exactly as we derive the ADT STACK [ACCOUNT] from the ADT pattern ST.ACK. Later chapters will explore the notion of genericity as applied to classes,and how to Chapter 10 and combine it with the inheritance mechanism. appendix B. Listing the functions After the TYPES paragraph comes the FUNCTIONS paragraph,which lists the operations applicable to instances of the ADT.As announced,these operations will be the prime component of the type definition-describing its instances not by what they are but by what they have to offer. Below is the FUNCTIONS paragraph for the STACK abstract data type.If you are a software developer,you will find the style familiar:the lines of such a paragraph evoke the declarations found in typed programming languages such as Pascal or Ada.The line for new resembles a variable declaration;the others resemble routine headers. FUNCTIONS ·pIt:STACK[G]×G→STACK[G] remove:STACK [G]+>STACK [G] item:STACK [GG empty:STACK [G]BOOLEAN ·new:STACK[GT Each line introduces a mathematical function modeling one of the operations on stacks.For example function put represents the operation that pushes an element onto the top of a stack. Why functions?Most software people will not naturally think of an operation such as put as a function.When the execution of a software system applies a put operation to a stack,it will usually modify that stack by adding an element to it.As a result,in the above informal classification of commands,put was a"command"-an operation which may modify objects.(The other two categories of operations were creators and queries)
132 ABSTRACT DATA TYPES §6.4 about instances of STACK and similar type patterns, with the understanding that this actually means instances of their generic derivations. Similarly, it is not quite accurate to talk about STACK being an ADT: the correct term is “ADT pattern”. For simplicity, this discussion will continue omitting the word “pattern” when there is no risk of confusion. The distinction will carry over to object-oriented design and programming, but there we will need to keep two separate terms: •The basic notion will be the class; a class may have generic parameters. •Describing actual data requires types. A non-generic class is also a type, but a generic class is only a type pattern. To obtain an actual type from a generic class, we will need to provide actual generic parameters, exactly as we derive the ADT STACK [ACCOUNT] from the ADT pattern STACK. Later chapters will explore the notion of genericity as applied to classes, and how to combine it with the inheritance mechanism. Listing the functions After the TYPES paragraph comes the FUNCTIONS paragraph, which lists the operations applicable to instances of the ADT. As announced, these operations will be the prime component of the type definition — describing its instances not by what they are but by what they have to offer. Below is the FUNCTIONS paragraph for the STACK abstract data type. If you are a software developer, you will find the style familiar: the lines of such a paragraph evoke the declarations found in typed programming languages such as Pascal or Ada. The line for new resembles a variable declaration; the others resemble routine headers. Each line introduces a mathematical function modeling one of the operations on stacks. For example function put represents the operation that pushes an element onto the top of a stack. Why functions? Most software people will not naturally think of an operation such as put as a function. When the execution of a software system applies a put operation to a stack, it will usually modify that stack by adding an element to it. As a result, in the above informal classification of commands, put was a “command” — an operation which may modify objects. (The other two categories of operations were creators and queries). FUNCTIONS • put: STACK [G] × G → STACK [G] • remove: STACK [G] STACK [G] • item: STACK [G] G • empty: STACK [G] → BOOLEAN • new: STACK [G] Chapter 10 and appendix B. → →
$6.4 FORMALIZING THE SPECIFICATION 133 See also“The im- An ADT specification,however,is a mathematical model,and must rely on well- perative and the ap-understood mathematical techniques.In mathematics the notion of command,or more plicative”,page generally of changing something,does not exist as such;computing the square root of the 351. number 2 does not modify the value of that number.A mathematical expression simply defines certain mathematical objects in terms of certain other mathematical objects:unlike the execution of software on a computer,it never changes any mathematical object. Yet we need a mathematical concept to model computer operations,and here the notion of function yields the closest approximation.A function is a mechanism for obtaining a certain result,belonging to a certain target set,from any possible input belonging to a certain source set.For example,if R denotes the set of real numbers,the function definition square_plus one:R→R square_plus_one (x)=x2+1 (for any x in R) introduces a function square plus one having R as both source and target sets,and yielding as result,for any input,the square of the input plus one. The specification of abstract data types uses exactly the same notion.Operation put, for example,is specified as PIt:STACK[G×G→STACK[G which means that put will take two arguments,a STACK of instances of G and an instance of G,and yield as a result a new STACK [G].(More formally,the source set of function put is the set STACK [G]X G,known as the cartesian product of STACK [G]and G;this is the set of pairs <s,x>whose first element s is in STACK [G]and whose second element x is in G.)Here is an informal illustration: Applying the put function put (stack) (element) (stack) With abstract data types,we only have functions in the mathematical sense of the term;they will produce neither side effects nor in fact changes of any kind.This is the condition that we must observe to enjoy the benefits of mathematical reasoning. When we leave the ethereal realm of specification for the rough-and-tumble of software design and implementation,we will need to reintroduce the notion of change; because of the performance overhead,few people would accept a software execution environment where every "push"operation on a stack begins by duplicating the stack. Later we will examine the details of the transition from the change-free world of ADTs to the change-full world of software development.For the moment,since we are study ing how best to specify types,the mathematical view is the appropriate one
§6.4 FORMALIZING THE SPECIFICATION 133 An ADT specification, however, is a mathematical model, and must rely on wellunderstood mathematical techniques. In mathematics the notion of command, or more generally of changing something, does not exist as such; computing the square root of the number 2 does not modify the value of that number. A mathematical expression simply defines certain mathematical objects in terms of certain other mathematical objects: unlike the execution of software on a computer, it never changes any mathematical object. Yet we need a mathematical concept to model computer operations, and here the notion of function yields the closest approximation. A function is a mechanism for obtaining a certain result, belonging to a certain target set, from any possible input belonging to a certain source set. For example, if R denotes the set of real numbers, the function definition square_plus_one: R → R square_plus_one (x) = x 2 + 1 (for any x in R) introduces a function square_plus_one having R as both source and target sets, and yielding as result, for any input, the square of the input plus one. The specification of abstract data types uses exactly the same notion. Operation put, for example, is specified as put: STACK [G] × G → STACK [G] which means that put will take two arguments, a STACK of instances of G and an instance of G, and yield as a result a new STACK [G]. (More formally, the source set of function put is the set STACK [G] × G, known as the cartesian product of STACK [G] and G; this is the set of pairs <s, x> whose first element s is in STACK [G] and whose second element x is in G.) Here is an informal illustration: With abstract data types, we only have functions in the mathematical sense of the term; they will produce neither side effects nor in fact changes of any kind. This is the condition that we must observe to enjoy the benefits of mathematical reasoning. When we leave the ethereal realm of specification for the rough-and-tumble of software design and implementation, we will need to reintroduce the notion of change; because of the performance overhead, few people would accept a software execution environment where every “push” operation on a stack begins by duplicating the stack. Later we will examine the details of the transition from the change-free world of ADTs to the change-full world of software development. For the moment, since we are studying how best to specify types, the mathematical view is the appropriate one. See also “The imperative and the applicative”, page 351. Applying the put function put ( , ) = (stack) (element) (stack)
134 ABSTRACT DATA TYPES $6.4 The role of the operations modeled by each of the functions in the specification of STACK is clear from the previous discussion: Function put yields a new stack with one extra element pushed on top.The figure on the preceding page illustrates put(s,x)for a stack s and an element x. Function remove yields a new stack with the top element,if any,popped;like put, this function should yield a command (an object-changing operation,typically implemented as a procedure)at design and implementation time.We will see below how to take into account the case of an empty stack,which has no top to be popped. .Function item yields the top element,if any. Function empty indicates whether a stack is empty;its result is a boolean value(true or false);the ADT BOOLEAN is assumed to have been defined separately. Function new yields an empty stack. The FUNCTIONS paragraph does not fully define these functions;it only introduces their signatures-the list of their argument and result types.The signature of put is STACK [G]XG→STACK [G indicating that put accepts as arguments pairs of the form <s,x>where s is an instance of STACK [G]and x is an instance of G,and yields as a result an instance of STACK [G].In principle the target set of a function (the type that appears to the right of the arrow in signature,here STACK [G])may itself be a cartesian product;this can be used to describe operations that return two or more results.For simplicity,however,this book will only use single-result functions. The signature of functions remove and item includes a crossed arrow >instead of the standard arrow used by put and empry.This notation expresses that the functions are not applicable to all members of the source set;it will be explained in detail below. The declaration for function new appears as just new:STACK with no arrow in the signature.This is in fact an abbreviation for new:-→STACK introducing a function with no arguments.There is no need for arguments since new must always return the same result,an empty stack.So we just remove the arrow for simplicity. The result of applying the function (that is to say,the empty stack)will also be written new,an abbreviation for new(),meaning the result of applying new to an empty argument list. Function categories The operations on a type were classified informally at the beginning of this chapter into creators,queries and commands.With an ADT specification for a new type T,such as STACK [G]in the example,we can define the corresponding classification in a more
134 ABSTRACT DATA TYPES §6.4 The role of the operations modeled by each of the functions in the specification of STACK is clear from the previous discussion: • Function put yields a new stack with one extra element pushed on top. The figure on the preceding page illustrates put (s, x) for a stack s and an element x. • Function remove yields a new stack with the top element, if any, popped; like put, this function should yield a command (an object-changing operation, typically implemented as a procedure) at design and implementation time. We will see below how to take into account the case of an empty stack, which has no top to be popped. • Function item yields the top element, if any. • Function empty indicates whether a stack is empty; its result is a boolean value (true or false); the ADT BOOLEAN is assumed to have been defined separately. • Function new yields an empty stack. The FUNCTIONS paragraph does not fully define these functions; it only introduces their signatures — the list of their argument and result types. The signature of put is STACK [G] × G → STACK [G] indicating that put accepts as arguments pairs of the form <s, x> where s is an instance of STACK [G] and x is an instance of G, and yields as a result an instance of STACK [G]. In principle the target set of a function (the type that appears to the right of the arrow in signature, here STACK [G]) may itself be a cartesian product; this can be used to describe operations that return two or more results. For simplicity, however, this book will only use single-result functions. The signature of functions remove and item includes a crossed arrow instead of the standard arrow used by put and empty. This notation expresses that the functions are not applicable to all members of the source set; it will be explained in detail below. The declaration for function new appears as just new: STACK with no arrow in the signature. This is in fact an abbreviation for new: → STACK introducing a function with no arguments. There is no need for arguments since new must always return the same result, an empty stack. So we just remove the arrow for simplicity. The result of applying the function (that is to say, the empty stack) will also be written new, an abbreviation for new (), meaning the result of applying new to an empty argument list. Function categories The operations on a type were classified informally at the beginning of this chapter into creators, queries and commands. With an ADT specification for a new type T, such as STACK [G] in the example, we can define the corresponding classification in a more →