Lecture
Это окончание невероятной информации про .
...
representation - must be closed (secret). When we begin building classes, we will encounter a fourth part, also secret - auxiliary properties needed only for the internal purposes of these programs.
Thus, using abstract data types as the source of modules gives us a practical, unambiguous guideline for applying information hiding in our designs.
The transition from ADTs to classes involves a significant change in style: the introduction of change and imperative arguments.
As you recall, the specification of abstract data types does not explicitly describe change, that is, using a term from theoretical computer science, it is applicative. All properties of an ADT are modeled as mathematical functions - this applies to constructors, queries, and commands alike. For example, the push operation for stacks is modeled by the command function:
put: STACK [G] × G STACK [G],
defining an operation that returns a new stack rather than modifying the existing one.
Classes abandon the purely applicative view of functions and redefine commands as operations that can modify objects. For example, the put operation will be defined as a procedure that takes an element of type G (the formal parameter) and modifies the stack by pushing the new element onto its top, without creating a new stack.
This change in style reflects the imperative sentiment prevailing in software development. (The term "operational" is sometimes used as a synonym for "imperative".) This will require modifying the ADT axioms. The stack axioms A1 and A4, which had the form
[x]. (A1) item (put (s, x)) = x
[x]. (A4) not empty (put (s, x))
will, in imperative form, turn into a clause called the routine's postcondition, introduced by the keyword ensure:
put (x: G) is -- Push x onto the top of the stack require ... Precondition (if any) ... do ... Corresponding implementation (if known) ... ensure item = x not empty end
Here the postcondition explains that, as a result of calling the routine put, the value of item will equal x (the pushed element), and the value of empty will be false.
Other axioms of the ADT specification give rise to an assertion known as the class invariant. We will look at postconditions, class invariants, and other reincarnations of ADT preconditions and axioms when we discuss assertions and design by contract (Section 11.10 "Relation to ADTs").
If you have carefully followed the main line of reasoning, starting from the lecture on modularity, that led us to abstract data types and then to classes, you may now be surprised. Having set out to obtain the best possible modular structure, we arrived at the conclusion that objects - or more precisely, object types - would be a better basis for modules than their traditional rivals, functions. This led to the next question: how to describe these object types. But when we answered it: they should be described in the form of abstract data types (and their practical stand-ins - classes), it turned out that we needed to base the description of data on ... the functions applied to it! Haven't we ended up in a vicious circle?
No. Object types, represented by ADTs and classes, remain the unchanging basis of modularization.
It is not surprising that both the object aspect and the functional aspect must appear in the final architecture of a system: no description of software issues can be considered complete if one of these components is omitted. The fundamental difference between OO methods and older approaches lies in the distribution of roles: object types are the unconditional winners when it comes to choosing the criteria for constructing modules. Functions are left only with the role of their servants.
In OO decomposition, no function exists on its own - every function is attached to some object type. This applies both at the design level and at the development level: no feature exists on its own, each of them is attached to some class.
We have already given a definition of constructing OO software: being quite general, it presents the method as follows: "base the architecture of any software system on modules derived from the types of objects that the system operates on". Staying within the bounds of this definition, we can now supplement it with a more technical definition:
Constructing OO software is building a software system as a structured collection of implementations (possibly partial) of abstract data types.
This definition will be our working definition. All of its components are important:
[x]. At its core lies the notion of an abstract data type.
[x]. To construct programs, we need not ADTs themselves (as a mathematical notion), but implementations of ADTs - a programming notion.
[x]. At the same time, these implementations need not be complete; the qualifier "possibly partial" allows the use of deferred classes as well, including, as an extreme case, a fully deferred class with no implementation at all.
[x]. A system is a collection of classes without singling out any main or responsible class or top-level program.
[x]. This collection is structured by virtue of two relations between classes: "being a client" and inheritance.
Let us now stress the importance of the ADT notion for areas lying outside the direct scope of its intended application.
The ADT-based approach tells us that serious intellectual inquiry should reject any attempt to understand the essence of things from within as useless, and should instead focus on understanding the properties of these things that are actually used. Don't tell me what you are, tell me what you have - what I can get from you. If we need to give this epistemological discipline a name, we would call it the principle of enlightened selfishness.
If I am thirsty, then an orange is something from which I can squeeze juice; if I am an artist, then color is something that can inspire my palette; if I am a farmer, then it is a product I can sell at the market; if I am an architect, then it is blueprints showing me how to design a new opera house; but if I am none of these, and make no use of an orange at all, then I should not speak of it, since the notion of "orange" does not even exist for me.
The principle of selfishness, which asserts that you are what you have, is an extreme expression of an idea that has played a central role in the development of science: the idea of abstraction, or the importance of separating notions. The two quotations given at the beginning of this lecture, each remarkable in its own way, express the importance of this idea. Their authors, Diderot and Stendhal, were writers rather than scientists, although it is clear that both had a good understanding of the essence of the scientific method. (Diderot was the ardent driving force behind the Great Encyclopedia, and Stendhal was preparing to enter the Polytechnic School, though he later decided he could find more suitable pursuits.) It is simply remarkable how well both quotations apply to the use of abstraction in software construction.
But there is something in the principle of selfishness beyond abstraction - the, at first glance shocking, idea that no property is worth mentioning if it offers no direct benefit to the speaker.
This leads us to consider the broader intellectual significance of our field.
Over the years, many articles and talks have suggested examining how software developers might benefit from studying philosophy, general systems theory, "cognitive science," or psychology. But for practicing software developers, the results turn out to be disappointing. If we set aside the universally applicable laws of rational (reasoned) inquiry, known to enlightened minds for many centuries already (at least since Descartes), which of course apply to computer science as to everything else, it sometimes seems that specialists in the above-mentioned disciplines could gain more by learning from software specialists than the other way around.
Software builders have taken on - with varying degrees of success - some of the most complex intellectual problems ever considered. Few engineering projects can rival in complexity the software projects containing many millions of lines that are routinely produced these days. Through no small amount of ambitious effort, the software community has achieved a precise understanding of such subjects and notions as size, complexity, structure, abstraction, taxonomy, concurrency, recursive inference, the distinction between description and prescription, language, change, and invariants. All of this has happened so recently and so intuitively that this professional community has not yet become aware of the epistemological consequences of its own activity.
Eventually, someone will appear who will explain what lessons the entire intellectual world can draw from the experience of software construction. There is no doubt that abstract data types will play an outstanding role in them.
The description of abstract data types presented above is quite sufficient for using ADTs within the scope of this book. (To supplement it, work through the exercises, which will help refine your understanding of this notion).
If, as I hope, ADTs have already won you over with their elegance, simplicity, and power, then you may well want to learn more about their properties, even ones that will not be used in the discussion of OO methods. The next few pages cover the following additional topics, which can be skipped on a first reading:
[x]. implicitness and its relation to the process of software construction;
[x]. the distinction between specification and design;
[x]. the distinction between classes and records;
[x]. possible alternatives to the use of partial functions;
[x]. the decision on the completeness or incompleteness of a specification.
The bibliographical references for this lecture point to more specialized literature on ADTs.
The implicit nature of abstract data types and classes, discussed above, reflects one of the important problems of software construction.
A perfectly legitimate question is the difference between a simplified ADT specification, using the function declaration
x: POINT REAL
y: POINT REAL
and a type declaration in a traditional programming language such as Pascal:
type
POINT =
record
x, y: real
end
At first glance, these two declarations appear equivalent: both state that two values x and y of type REAL are associated with the type POINT. But there is an essential, if subtle, difference between them:
[x]. A record in Pascal is complete and explicit: it shows that the POINT object consists of two data fields and nothing else.
[x]. The ADT function declarations carry no such meaning. They show that an object of type POINT can be queried for the values of its x and y, but they do not exclude other queries, for example about the mass and velocity of the point in a kinematic application.
From a simplified mathematical point of view, the Pascal declaration given above can be regarded as defining the mathematical set POINT as a Cartesian product:
POINT REAL × REAL,
where the symbol means "is defined as" ("equal by definition"), and it fully determines POINT. In contrast, the ADT specification does not explicitly define POINT by means of such a mathematical model as a Cartesian product; it merely implicitly characterizes POINT by listing the two queries applicable to objects of this type.
Given the specification of some notion, one may wish to move it from the implicit world to the explicit one by identifying the notion with the Cartesian product of the simple queries applicable to it - for example, one might want to identify points with pairs. Such a process of identification can be regarded as defining the transition from analysis and specification to design and implementation.
The preceding observation helps clarify one of the central questions arising in the study of software: the distinction between the initial stage of software development - its specification, also called analysis - and the later stages such as design and implementation.
The literature on software development usually explains this as the difference between "defining the problem" and "building its solution". While correct in principle, such an explanation is not always applicable in practice, and it is sometimes hard to tell where specification ends and design begins. Even among researchers, people readily criticize each other on this topic: "you advertise language x as a specification language, but it is actually meant for design". The gravest insult is to accuse some notation of catering to implementation (more on this in one of the following lectures).
The definition given above provides a more precise criterion: to cross the Rubicon between specification and design is to move from the implicit to the explicit, in other words:
Definition: transition from analysis (specification) to design
To move from specification to design is to identify each abstraction with the Cartesian product of its simple queries.
The subsequent transition - from design to implementation - is simply a move from one explicit form to another: the form used in design is more abstract and closer to mathematical notions, while the form used in implementation is more concrete and closer to the computer, but both are explicit. This transition is less dramatic than the previous one - indeed, as we read on it will become clear that object technology almost erases the distinction between design and implementation. With a good OO notation system, what would often be regarded as designs in the non-OO world is directly executed by our computers (via compilers).
Another remarkable property of object technology is that it lets us keep implicit descriptions for much longer than other approaches do. In later lectures we will introduce a notation that lets us define a class in the form:
class POINT feature x, y: REAL end
This looks suspiciously similar to the Pascal record definition given above. But despite the outward resemblance, a class definition is different - it is implicit! This implicitness shows up under inheritance: the author of the class, or (even more interestingly) someone else entirely, can at any moment define a new class, for example:
class MOVING_POINT inherit POINT feature mass: REAL velocity: VECTOR [REAL] end
which extends the original class in a completely unplanned way. Then a variable (or entity, to use terminology introduced later) of type POINT, declared as
p1: POINT
can be attached not only to an object of type POINT, but also to an object of any descendant of that type, for example an object of type MOVING_POINT. This can happen, in particular, through "polymorphic assignments" of the form:
p1 := mp1
where mp1 has type MOVING_POINT.
These possibilities illustrate the implicitness and openness of a class definition: the corresponding instances represent not only points in the narrow sense, i.e. direct instances of the class POINT, but also instances of any class describing notions derived from the original class.
The ability to define program elements (classes) that are immediately usable (through inheritance) while remaining implicit is one of the main innovations of object technology, and it directly answers to the Open-Closed principle. All the consequences that follow from it will be unfolded in later lectures.
One of the technical devices used in this lecture may have caused some surprise - the use of partial functions. It is tied to the unavoidable problem of applying, within some specification, operations that are not defined everywhere. But are partial functions the best solution to this problem?
Of course, this is not the only possible solution. Another approach, which comes to mind and is indeed used in some works on ADTs, is to turn a partial function into a total one by introducing a special "error" value for cases where the function is applied to unsuitable arguments.
Every type T is augmented with an "error" value. Let us denote it by w T . Then, for every function f, the signature
f: ... Input types ... T
states that every application of f to an object for which the corresponding computation cannot be performed will yield the value w T .
Although this method is used, it leads to mathematical and practical inconveniences. The problem is that such special values are quite eccentric creatures, capable of considerably complicating the lives of innocent mathematical entities.
Suppose, for example, that we consider stacks of integers - instances of the type STACK [INTEGER], where INTEGER is the ADT whose instances are integers. Although our example does not require writing out the full specification of INTEGER, this ADT must model the basic operations (addition, subtraction, "less than", and so on) defined on the mathematical set of integers. The axioms of this ADT must express the usual properties of integers. Here is one such typical property: for every integer n:
[Z1]
n + 1 n
Now let n be the result of querying the top element of an empty stack, i.e. the value of the expression item (new), where new is an empty stack of integers. In this query, n must receive the special value w INTEGER . What, then, should the value of the expression n+1 be? If the only values available to us are ordinary integers and w INTEGER , then we are forced to choose w INTEGER as the answer:
wINTEGER + 1 = wINTEGER.
This is the only acceptable choice. If we assigned w INTEGER +1 any other value, a "normal" number q, this would mean that after attempting to access the top of an empty stack and getting an erroneous value as the result, we could magically erase all memory of that error simply by adding one to the result!
But choosing w INTEGER as the value of n + 1 when n equals w INTEGER violates the property Z1 stated above. In general, the expression w INTEGER +p will equal w INTEGER for any p. This means that the modified data type (INTEGER, augmented with an error element) requires a new system of axioms explaining that every operation on integers returns the value w INTEGER if at least one of its arguments equals w INTEGER . Similar changes would be required for every type.
The resulting complication does not seem justified. We cannot change the specification of integers just to model each individual data structure (in our case, stacks). When partial functions are used, the situation is simpler. Of course, for every expression containing partial functions, one has to check that their arguments satisfy the corresponding preconditions. Once that check has been completed, the axioms can be applied without hindrance. This does not require modifying the existing systems of axioms.
Another question that may be troubling you: is there any way to make sure that a specification describes all the necessary properties of the objects it is meant to represent? Students who need to write their first specifications (for example, doing the exercises at the end of this lecture) often come up with a similar question: "How do I know that I have already specified enough properties and can stop?"
In more general form, the question is this: is there a method for determining the completeness of an ADT specification?
If we ask the question directly in this form, the answer is simple - no. It is clear that, for a formal specification, saying that it is complete means claiming that it covers all the necessary properties, but this only makes sense relative to some reference document in which all these properties are listed. We then face two equally unsatisfying situations:
[x]. If the reference document is informal (for example, a natural-language requirements document, or simply the text of an exercise), the lack of formality prevents any systematic attempt to verify that the specification meets all the requirements described in that document.
[x]. If, on the other hand, the reference document is formal, and we can use it to check the completeness of our specification, this simply pushes the problem further back: how can we be sure that the reference document itself is complete?
Thus, in this trivial form, the question of completeness is not interesting. But there is a more useful notion of completeness, corresponding to the meaning of the word in mathematical logic. For a mathematician, a theory is complete if its axioms and inference rules are powerful enough to prove the truth or falsity of any formula expressible in the language of that theory. Although this notion of completeness is more limited, it is intellectually quite satisfying, since it shows that if a theory allows us to express some property, it also allows us to determine whether that property holds.
How can this idea be carried over to ADT specifications? Here, the "language of the theory" is the set of well-formed expressions, that is, the expressions that can be built using the ADT's functions applied to arguments of the appropriate types. For example, using the specification of the ADT STACK, and assuming that x is a well-formed expression of type G, we can give the following well-formed expressions:
new
put (new, x)
item (new) - if this seems strange, see the comments below.
empty (put (new, x))
stackexp - a complex expression defined earlier.
However, the expressions put (x) and put (x, new) are not well-formed, since they do not conform to the rule: put must always have two arguments - the first of type STACK [G] and the second of type G.
The third boxed example, item (new), does not specify any meaningful computation, since the argument new does not satisfy the precondition for item. Although this expression is well-formed, it is not valid. Here is the precise definition of this notion.
Definition: valid ADT expression
Let f(x1 , ... , xn) be a well-formed expression containing one or more functions of some ADT. This expression is valid if and only if all of its arguments xi are (recursively) valid and their values satisfy the precondition of f, if it has one.
"Valid" should not be confused with "well-formed". "Well-formed" is a structural property, indicating that the functions occurring in the expression have the correct number of arguments of the appropriate types, while validity, which only well-formed expressions can possess, means that the expression in question specifies a meaningful computation. As we have seen, the expression put (x) is not well-formed (so it is meaningless to ask whether it is valid), while the expression item (new) is well-formed but not valid.
A well-formed but invalid expression is similar to a program that compiles (since it was built according to the syntax requirements of the programming language and satisfies the type constraints it imposes), but crashes at run time because it performs some illegal operation, for example dividing by 0 or popping an element off an empty stack.
Of particular interest from the point of view of completeness are query expressions, whose outermost function is a query. Here are examples of such expressions:
empty (put (put (new, x1), x2)) item (put (put (new, x1), x2)) stackexp
A query expression specifies a value that (if it is defined) belongs not to the ADT being defined, but to some other, previously defined type. Thus, the first expression given above has a value of type BOOLEAN, while the second and third have the type G of the formal parameter for the stack elements - for example, if we are considering the ADT STACK [INTEGER], this would be the type INTEGER.
Query expressions represent the external observations that can be made about the results of some computation using instances of the new ADT. If the specification of this ADT is good, it should let us determine whether these results are defined, and if so, what they are. It appears that the stack specification has this property, at least for the three expressions presented in the example, since it lets us establish that all these expressions are defined, and their values can be obtained using the axioms:
empty (put (put (new, x1), x2)) = False item (put (put (new, x1), x2)) = x2 stackexp = x4
These observations, carried over to arbitrary ADT specifications, lead to a pragmatic notion of completeness known as sufficient completeness, meaning that the specification contains axioms strong enough to determine, for any query expression, its result as some simple value.
Let us give a precise definition of sufficient completeness. (Readers not inclined toward mathematics may skip the rest of this section).
Definition: sufficient completeness
The specification of an ADT T is sufficiently complete if and only if the axioms of its theory allow us, for every expression expr, to settle the following questions:
[x]. (S1) Determine whether expr is valid.
[x]. (S2) If expr is a query expression and its validity has been established in item S1, represent the value of expr in a form that includes no values of type T.
In S2, the expression expr has the form f(x1 , ..., xn), where f is a query-type function such as empty and item for stacks. S1 tells us that expr has a value, but that is not enough; we want to know what that value is, expressed in terms of values of other types (in the stack example, these are values of types BOOLEAN and G). If the axioms are strong enough to always answer this question, the specification is sufficiently complete.
Sufficient completeness demonstrates that no important property has been left out of our specification. It can therefore be regarded as an answer to the question posed above: how do we know when to stop looking for new properties while building a specification? In practice, it is a good idea to perform this check, at least informally, for any ADT specification you write - start with the solutions to the exercises given in this lecture. Often, a formal proof of sufficient completeness can be obtained; the proof given below for the STACK specification is a model that can be followed in many cases.
Item S2 optimistically speaks of a single value of expr, but what if the axioms lead to two or more values? That would make the specification useless. To rule out this situation we need one more property, called consistency in mathematical logic:
Definition: ADT consistency
An ADT specification is consistent if and only if, for every well-formed expression expr, its axioms allow us to derive at most one value.
These two properties are mutually complementary. For every query expression, we want to derive exactly one value: at least one (sufficient completeness), but no more than one (consistency).
(This section and the rest of this lecture contain supplementary material, and their results are not needed for the rest of the book).
Sufficient completeness of ADT specifications is, in general, an algorithmically undecidable problem. In other words, there is no general proof method that could, given an ADT specification, determine its sufficient completeness in finite time. Consistency is likewise undecidable in general.
Despite this, it is often possible to prove sufficient completeness and consistency for a specific ADT specification. To satisfy the curiosity of mathematically inclined readers, we conclude this lecture with a proof that the STACK specification is indeed sufficiently complete. The proof of its consistency will be left as an exercise.
To prove the sufficient completeness of the stack specification, we need to devise an effective rule for solving the tasks S1 and S2 stated above, in other words a rule that will let us, for any stack expression e:
[x]. (S1) Determine whether e is valid.
[x]. (S2) If item S1 has established the validity of e and its outermost functions are item or empty (i.e. the query functions), represent the value of e using values of types BOOLEAN and G, without any reference to values of type STACK [G] or to functions from the STACK specification.
To begin with, we will only consider well-formed expressions that do not include either of the two query functions item and empty, i.e. expressions built only from the functions new, put, and remove. Thus, at this stage we will only be concerned with task S1 (establishing whether the expression is defined). The query functions and S2 will be considered later.
The rule for solving task S1 is given by the following property:
The Valid Weight Rule
A well-formed stack expression e, containing neither item nor empty, is valid if and only if its weight is non-negative and each of its subexpressions is (by induction) valid.
Here the "weight" of an expression represents the number of elements in the corresponding stack; this value also equals the difference between the number of nested occurrences of the functions put and remove. Let us give a precise definition of this notion:
Definition: weight
The weight of a well-formed stack expression containing neither item nor empty is defined by induction as follows:
[x]. (W1) The weight of the expression new is 0.
[x]. (W2) The weight of the expression put (s, x) is ws + 1, where ws is the weight of s.
[x]. (W3) The weight of the expression remove (s) is ws- 1, where ws is the weight of s.
Informally, the valid weight rule states that a stack expression is valid if and only if it, together with each of its subexpressions, contains no fewer put operations (inserting elements into the stack) than remove operations (popping elements off the top of the stack). If we regard such an expression as representing some computation on a stack, this means that we will never attempt to pop more elements than we pushed. Recall that at this stage we are focusing on the functions put and remove, leaving the queries item and empty aside.
The intuitively stated rule looks correct, but we still need to prove that it holds. It is convenient to introduce one more auxiliary rule and prove the validity of both rules at the same time:
The Zero Weight Rule
Let e be a well-formed and valid stack expression containing neither item nor empty. Then empty (e) is true if and only if the weight of e is 0.
The proof uses induction on the nesting level (the maximum number of nested pairs of parentheses) of the expression. For ease of reference, let us recall the axioms relating to the function empty:
Stack Axioms
For all x: G, s: STACK [G]
[x]. (A3) empty (new)
[x]. (A4) not empty (put (s, x))
At nesting level 0 (no parentheses), the expression e must coincide with new, so its weight is 0 and it is valid, since new has no preconditions. Axiom A3 states that empty (new) is true. This gives us the base case of the induction for both the valid weight rule and the zero weight rule.
Induction step: assume that both rules hold for all expressions with nesting level at most n. We need to prove that they then hold for any expression e with nesting level n+1. Since our expressions currently contain no query functions, e must have one of the following two forms:
E1 · e = put (s, x) E2 · e = remove (s)
where x has type G, and the nesting level of s equals n. Let ws be the weight of s.
In case E1, since put is an everywhere-defined function, e is valid if and only if s is valid, i.e. (by the induction hypothesis) if and only if s and all its subexpressions have nonnegative weights. But this is equivalent to e and all its subexpressions having nonnegative weights, which proves the correct-weight rule in this case. Moreover, e has a positive weight ws+1, and (by axiom A4) is nonempty, which proves the zero-weight rule.
In case E2, the expression e is valid if and only if the following two conditions hold:
EB1 _ s and all its subexpressions are valid.
EB2 _ not empty (s) (this is the precondition for the remove function).
By the induction hypothesis, condition EB2 means that the weight of s, ws, is positive, or, equivalently, the weight of e, equal to ws - 1, is nonnegative. Therefore, e satisfies the correct-weight rule. To prove that it also satisfies the zero-weight rule, we must show that e is empty if and only if its weight equals 0. Since the weight of s is positive, s must contain at least one occurrence of put, which is also contained in e. Consider the outermost occurrence of put in e; this occurrence is located directly inside remove (since remove is at the outermost level of e). This means that e has a subexpression (which may coincide with e itself) of the form
remove (put (stack_expression, g_expression)),
which, by axiom A2, can be reduced simply to stack_expression. After performing this substitution, the weight of e decreases by 2, and the resulting expression, which has the same value as e, satisfies the zero-weight rule by the induction hypothesis. This proves the induction statement in case E2.
This proof shows, incidentally, that in any well-formed expression that does not contain the query functions item and empty, all occurrences of remove can be eliminated, i.e. one can obtain, by applying axiom A2 everywhere it is possible, some canonical form containing only put and new. For example, the expression:
put (remove (remove (put (put (remove (put (put (new, x1), x2)), x3), x4))), x5)
has the same value as the canonical form:
put (put (new, x1), x5).
Let us give this mechanism a name and provide its definition:
Every well-formed and valid stack expression that does not contain the query functions item and empty has an equivalent canonical form that does not contain the function remove (i.e. consists only of the functions put and new>). This canonical form is obtained by applying stack axiom A2 for as long as possible.
Thus, we have completed the proof of sufficient completeness, but only for expressions that do not contain query functions, and hence only for property S1 (checking the validity of an expression). To complete the proof, we need to consider expressions that include query functions, and discuss problem S2 (finding the values of query expressions). This means that we need some rule for determining the validity and value of any well-formed expression of the form f(s), where s is a well-formed expression, and f is either item or empty.
This rule and the proof of its correctness also use induction on the nesting level. Let n be the nesting level of s. If n=0, then s can only be new, since the other functions require arguments and therefore contain at least one pair of parentheses. Then, for both query functions, the situation is clear:
[x]. empty (new) is valid and has the value true (by axiom A3);
[x]. item (new) is invalid, since the precondition of item requires not empty (s) to hold.
Induction step: suppose s has nesting level n of at least 1. If for some subexpression u of s the outer function is item or empty, then the nesting level of u does not exceed n-1, which by the induction hypothesis lets us determine the validity of u and, if u is valid, obtain its value by applying the axioms. After performing the substitutions for all such subexpressions, we obtain for s an equivalent form containing only the functions put, remove and new.
Next we use the idea of the canonical form introduced above to get rid of all occurrences of remove, so that the resulting form for s will include only the functions put and new. The case where s is simply new has already been considered; what remains is the case where s has the form put(s', x) . In this case, for the two expressions under consideration we have:
[x]. empty (s) is valid and by axiom A3 the value of this expression is false;
[x]. item (s) is valid, since the precondition not empty (s) for item holds; from axiom A1 it follows that the value of this expression equals x.
This completes the proof of sufficient completeness, since we have shown the validity of the set of rules - the correct-weight rule and the canonical-reduction rule, which allow us to determine the validity of a given stack expression, and for a valid query expression, to determine its value in terms of the values of types BOOLEAN and G.
[x]. The theory of abstract data types (ADT) reconciles the need for precise and complete specifications with the desire to avoid unnecessary detail in the specification.
[x]. The specification of an abstract data type is a formal mathematical description, not program text. It is applicative, i.e. it does not explicitly include changes.
[x]. An ADT may be generic, and it is defined by functions, axioms and preconditions. Axioms and preconditions express the semantics of the given type and are important for its complete and unambiguous description.
[x]. Partial functions form a convenient mathematical model for describing operations that are not everywhere defined. Each partial function has a precondition specifying the condition under which it will produce a result for a given specific argument.
[x]. An OO system is a collection of classes. Each class is based on some abstract data type and provides a partial or complete implementation of that ADT.
[x]. A class is effective if it is fully implemented; otherwise it is called deferred.
[x]. Classes should be designed in the most general form that allows reuse; the process of combining them into a system often proceeds bottom-up.
[x]. Abstract data types are implicit rather than explicit descriptions. This implicitness, which also means openness, carries over to the whole OO method.
[x]. There is no formal definition of the intuitively clear notion of "completeness" of an abstract data type specification. The rigorously defined notion of sufficient completeness generally provides a satisfactory answer. Although there is no method for establishing sufficient completeness for an arbitrary specification, it is often possible to prove it for specific specifications; the proof of sufficient completeness for the stack specification given in this lecture can serve as a model for other cases as well.
E6.1 Points. Write a specification defining an abstract data type POINT, modeling points in the plane in plane geometry. This specification should reflect the following aspects: Cartesian and polar coordinates, rotations, translations, distance from the origin, distance to another point.
Describe this problem as a set of abstract data types: LEAGUE_ADT, BOXER, BOUT. (Hint: do not explicitly introduce the notion of "rank", but model it using a "superior_to" function expressing the superiority relation on the set of the league's boxers.)
How would you add functions representing the operations of opening and closing an account? (Hint: these functions are functions of another ADT).
E6.5 Names. Design an abstract data type NAME that takes into account the various components of a person's full name.
Define a general ADT ALLOCATOR, covering both stacks and queues.
Consider a mechanism for defining more specialized ADT specifications (such as stacks and queues) by referring to general specifications such as the allocator specification. (Hint: look at the inheritance mechanism studied in the following lectures).
Study the ADT specification you wrote as a solution to one of the previous exercises, and try to prove that it is sufficiently complete. If it is not sufficiently complete, explain why and show how it can be fixed or extended to make it sufficiently complete.
Часть 1 6. Abstract Data Types (ADT)
Часть 2 Moving Toward a More Imperative Point of View - 6.
Comments