Object-Z is not a 'pure' Object Oriented Language

Alena Griffiths and Gordon Rose [in University of Queensland SVRC Technical Report 95-38, 1995, section 3.1.1] state:

The development of Object-Z as an extension of Z pollutes the "object-orientedness" of Object-Z insofar as it complicates the type structure with types other than classes.

By this, they presumably mean that the integers, sequences, cartesian products, and so on, of Z are not classes. Though this is rather obvious, it had not occurred to me until I read Griffiths and Rose's paper. It means that Object-Z is what Bertrand Meyer would call a hybrid 'object-based' language (like C++ and Ada) rather than a 'truly object-oriented' language like Smalltalk or Eiffel.  This then leads one to ask what a 'truly object-oriented' specification language would look like.  Presumably it would have all  the advantages of simplicity and orthogonality that Smalltalk and Eiffel have over C++ and Ada.  What we really need is a specification language in which the object oriented features arise naturally from the logic and are not cobbled on, almost as an after thought, as they are in Object-Z, Z++ and other object oriented specification languages.

What do UML Class Diagrams mean?

Consider the following UML class diagram:



What does this diagram say? What does it mean?  What does it actually constrain? 

This is not just an idle philosophical question; it goes to the very root of the formal specification of software systems.  Get the answer to this wrong and you condemn yourself to being overwhelmed by unnecessary complexity when you try to reason about non-trivial systems.  Get it right and, while you will still have to deal with complexity, at least this will only be proportional to the inherent complexity of the system.

There is a lot of UML literature which purports to give a semantics to the UML.  However, these forms of semantics are either expressed in words, and are therefore ambiguous and imprecise, or else are minutely detailed mathematical models of box and arrow diagrams intended for the implementors of UML diagramming tools.  Both of these are inadequate if what you want to do is to reason about specifications.

I suggest that the semantics of the above diagram is best expressed using first-order predicate logic as follows:

∀a . a∈A ⇒ (a∈B ∧ f(a)∈C)

It would also be possible to express this in terms of the subset relationship and relational image:

A⊆B ∧ f(|A|)⊆C

However, I prefer to make the quantifier and its variable explicit (the latter is analogous to the implicit self variable in object oriented class definitions).  I also prefer to use Lamport's prefix layout for conjuctions and disjunctions.  This is the way I would normally write this specification:

∀a . a∈A ⇒
    ∧ a∈B
    ∧ f(a)∈C

Note that this does not require that any A's (or B's or C's) actually exist.  It only requires that if they do then they must be constrained in the above way (ie: they must also be members of B, and when function f is applied to them it must return a member of C).

Note also that the above specification is extendible.  The use of implication allows us to later add further constraints.  This is consistent with the idea that UML diagrams are partial views of the complete system.

Also, the specification says nothing about the value returned by the function f when it is applied to a value that is not in A.  In that case the returned value is unconstrained (for example, we cannot say whether it is in C or not in C).

HTML and All That

I am currently reading Designing with Web Standards by Jeffrey Zeldman (New Riders, 2003).  After reading part I of this book I feel fully justified in my long-held aversion to web programming.  Even now it is apparently only possible to get reasonably consistent results across all browsers by resorting to ugly hacks. 

The immaturity of the whole field reminds me of programming the half-baked microcomputer BASIC interpreters of the early 1980s: some things that you want to do are either impossible or else can only be done in an extremely inefficient way.  Well known principles such as "Keep each item of information in one and only one place" and "Use symbolic names for numerical constants" are just ignored.  However, I suppose this immaturity is only to be expected in a field that has gone through an exponential growth phase during which new people have been coming into the field faster than good programming principles spread.

Zeldman's book provides a good account of both the horrors and the W3C's proposed cures and gives lots of practical examples.  However, it is not an introductory book: it assumes a familiarity with HTML, XHTML and CSS.

Buzzards over Reading

Last Friday evening, as I was going out with Zoe and Liz, I saw a large bird out of the corner of my eye.  I assumed, from its size, that it must be a grey heron but it disappeared behind a nearby block of flats before I could get a good look at it.  I walked on a few steps so that I would be able to see it again as it reappeared round the side of the flats but instead, it came back over the roof, and then it was clear that it wasn't a heron but a large bird of prey, dark all over except for white areas on the undersides of the wings.  Its tail was narrow like that of a kestrel, but the bird was much larger than any kestrel.  Reference to the BWP-CE confirmed my suspicion that this must have been a buzzard (Buteo buteo).  Buzzards vary in the darkness of their plumage.  This one must have been one of the darker ones.

I have seen birds that I suspected were buzzards before, but they have always been high in the sky, far too high to see any detail on them.  This one was at low level and only about 30 metres away and the markings were clear.  Zoe and Liz saw it too.

Earlier this year, while I was at work, Liz and Zoe saw a large bird of prey, that might have been a buzzard, eating a wood pigeon on our back lawn.  However, neither of them was able to provide a good enough description to allow me to identify it.  Later that day that bird carried the dead pigeon up onto our roof, presumably to be able to finish its meal without being disturbed.  By the time I got home all that was left was a scatter of pigeon feathers on the lawn.

Several years ago I was walking with Zoe along Kennetside in central Reading when we heard a mewing sound from above and looked up to see a large bird of prey high up, apparently being mobbed by some gulls.  That too was probably a buzzard, as their characteristic call is a mewing sound.

Egyptian Geese on Reading University Lakes

This afternoon I went for a walk with Liz  and Zoe around the three lakes in the grounds of Reading University.  These are set in an area of parkland that is just 10 minutes walk from where we live.  Liz often takes Zoe there to feed the ducks and geese after school.

For the past five years --and probably longer-- there has been a pair of Egyptian geese (Alopochen aegyptiacus) living on the larger of these lakes.  These are fairly weird looking birds which come in two forms: a darker rufous form with dark brown eye-patches and a lighter grey form with much fainter eye-patches. Our pair consists of one rufous and one grey.  The grey one --probably the female-- has a deformed leg and always seemed rather sickly, so last year I was surprised when the pair successfully reared three chicks.  This year they reared two more, and two of the previous year's offspring also reared a chick between them.  That makes eight in all, but Zoe tells me that one of last year's brood has either died or  else has left the area (presumably in search of a mate).  That leaves seven.  This afternoon we saw five of the extended family during our walk.  All of the chicks, both this year's and last, appear to be of the rufous form (this suggests that the grey form is genetically recessive).

I understand that there are only about 900 Egyptian geese in the UK and that 90% of these live in the wetlands of Norfolk. This means that our seven Egyptian geese represent about one thirteenth of the UK population outside Norfolk! (Of course, this assumes that the rest of the UK population has stayed the same.)