1 INTRODUCTION This is the fifth article in a regular series on object-oriented type theory, aimed specifically at non-theoreticians. The series has been investigating the notion of simple object types and subtyping from the Figure 1: Dimensions of Type Checking However, component compatibility is not just a matter of observing the conventions on type signatures. An object could offer all the expected operations, but still execute in a completely perverse way (see earlier article [3]). It is equally important to know whether a component All of these approaches are incomplete realisations of the more fundamental 2 INITIAL AND FINAL ALGEBRAS Mathematicians have been experimenting with notions of abstract types and classification since the early part of the 20th century. Much of this work falls within the remit of In the universe of algebras, families of algebras exist in which elements and operations that are distinct in one algebra become merged and indistinguishable in other algebras. Consider that if "+" is an abstract operation with just the property of 3 AXIOMATIC SEMANTICS When defining an algebraic type, the first concern is to establish under what semantics the axioms of the algebra will be interpreted. The Ordinal type The onus is on showing that the first() element is distinct from any successor succ(x), that any element x is distinct from its immediate successor succ(x), and that by induction all the elements of the type are eventually distinct, such that Ordinal is inhabited by a series of monotonically increasing elements: first(), succ(first()), succ(succ(first())) ... We change our approach to define the behaviour of object types. The Stack algebra below is defined using In the signature of Stack's operations, the use of " logical 4 INDUCTIVE DEFINITIONS The strategy for defining the behaviour of an object type uses an inductive approach, similar to recursive function definition in a functional programming language. In the axioms defining the meaning of The equations always relate pairs of methods on the left-hand side and assert that a nested invocation of these methods is equivalent to something else on the right-hand side (think of Stack axioms (1) and (2) as being "equivalent to true" on the right-hand side). How do you decide which pairs of methods to relate; and how do you know when sufficient axioms have been defined? If too many axioms are supplied, a theorem prover might waste time exploring redundant solutions that could be derived from other axioms. To help with this problem, the functions of the type are sometimes divided into three groups: - constructors - the smallest set of functions returning the type, which, taken together, can generate
*every single instance*of the type;
- transformers - the remaining functions which return the type, but which are non-primitive in the sense that they can be defined in terms of primitive constructors;
- observers - functions returning something other than the type, typically because they inspect part of the type or compute some value from it.
Note that Thereafter, the maximum number of axioms to define is decided. You need no more than an axiom for 5 DEDUCTIVE REASONING Let us now assume that we wish to derive some property of Stacks. For example, what is the
To simplify this, we look for axioms which relate suitable pairs of operations on their left-hand side, and substitute the corresponding equivalent expressions on their right-hand side. Working backwards from the end of the expression, and given s : Stack: - There is no axiom for s.pop().size(); but this is not an omission, since pop is not a primtive constructor and we can derive its meaning elsewhere. Instead, we look further.
- There is an axiom (6) with s.push(e).pop() on the left-hand side, so if we make the substitutions: s newStack().push(e1), giving the simplification:
- There is an axiom (4) with s.push(e).size() on the left-hand side, so if we make the substitutions: s 1+newStack().size(), giving the simplification:
- Finally, there is an axiom (3) giving newStack().size() directly:
and the final answer 1+0 = 1 is obtained using the algebra for Natural numbers in a similar fashion. This is the right answer and, hopefully, the one the reader expected! 6 ERRORS AND DEFERRED DEFINITIONS The two axioms omitted from Stack's equations were those relating: newStack().top() and newStack().pop(). This is because the meanings of There may be other valid reasons for "saying less about" a type than just to specify error cases. Consider first that a Queue type looks quite similar to a Stack, except that some of its functions behave in a slightly different way: The differences are in axioms (5) and (6), which assert FIFO properties for a Queue, contrasting with the LIFO properties asserted above for a Stack. Queue's equations also demonstrate how a right-hand side can be split into several cases, using Given that Queue and Stack are It is clear that both Stack and Queue satisfy the above definition, since they have the identical signatures, and obey the identical axioms (1) - (4). The fact that axioms (5) and (6) are missing means that, at the level of generality described by 7 UNDERSPECIFICATION AND SUBTYPING The rules governing axioms and semantic subtyping follow from this. If a type is underspecified, then a subtype may be created by adding suitable axioms giving the missing meanings of the underspecified operations. Note that Stack and Queue define mutually exclusive axioms (5) and (6), such that one could never be a subtype of the other; yet both are semantic subtypes of Dispenser, since they only add to Dispenser's existing axioms and do not violate any of them. Consider now that, in just one case, Stacks and Queues actually do behave identically in regard to These two axioms express, for both Stacks and Queues, that if you Finally, we can show a relationship between semantic and syntactic subtyping. Why does adding axioms, or strengthening axioms to cover more cases, create a subtype? Consider defining a set S by comprehension in relation to a set T, such that S contains all those elements in T which satisfy the extra axiom p(x): It is clear that, if all elements of T pass the test p(x), then S = T. However, if some elements of T fail the test, then S T, and this also means that S is a subtype of T [2]. 8 CONCLUSION We have developed an algebraic calculus for reasoning about the - strengthening an
*invariant*is identical to strengthening the axioms of an algebra, since the invariant applies constantly to the object type as a whole;
- strengthening a
*method postcondition*corresponds either to strengthening the axioms on the result-type of the method, or strengthening the axioms on the object type itself; or possibly to both of these;
- strengthening a
*method precondition*corresponds either to strengthening the axioms on the argument-types of the method, or strengthening the axioms on the object type itself; or possibly to both of these.
Since there is a direct relationship between axiom strengthening and subtyping, we can immediately apply our existing object subtyping rules [2] to derive subtyping rules governing the strengthening, or weakening of assertions. Recall that an object type which adds to the methods of another object type is a subtype. The subtype will define the semantics of the extra methods, providing more axioms, which is consistent with being a subtype. Some of these extra axioms may appear as strengthened invariants, which is also consistent. Apart from this, an object type may sometimes replace methods, so we must consider under what conditions this results in a subtype. A method is a valid replacement for another if it obeys the function subtyping rule [2]. In particular, the subtype method's arguments must be of the same, or more general (but not more restricted) types; and its result must be of the same, or a more restricted (but not more general) type. Translating this into assertions, the method's preconditions may
REFERENCES [1] A. J. H. Simons: [2] A. J. H. Simons, [3] A. J. H. Simons, [4] D. Harel and A. Naamad, [5] J. Warmer and A. Kleppe, [6] C A R Hoare, [7] B. Meyer,
Cite this column as follows: Anthony J.H. Simons: "The Theory of Classification, Part 5: Axioms, Assertions and Subtypes", in Journal of Object Technology, vol. 2, no. 1, January-February 2003, pp. 13-21. http://www.jot.fm/issues/issue_2003_01/column2 |