Undefined Values should remain Undefined

In "On Using Conditional Definitions in Formal Theories" J. R. Abrial and L. Mussat [in D. Bert et al (Eds.), ZB2002, Lecture Notes in Computer Science. pages 242-269, Springer, 2002] review various approaches to handling undefined values.  One of these, approach (3) on page 247, involves "claiming that a term of the form E/0 denotes a genuine real number, but that this number is unknown".  Abrial and Mussat go on to express the opinion that it is "hard to accept" that "3/0 denotes a real number".

I agree. In my approach 3/0 denotes a value but we cannot tell what that value is, not even whether it is a real number or not:  It is completely undefined.  The requirement that the value must be a real number appears to arise from the inappropriate enforcement of typing requirements.  The problem is that the type invariant is being (incorrectly) enforced in the post-condition, even when the pre-condition does not hold.  For example, consider:

∀x,y. x∈R ∧ y∈R ⇒
    (x/y)∈R

Here x/0 is required to always be in R (assuming x and y are in R), whereas what we really want is for the (x/y)∈R to be guarded as follows:

∀x,y. x∈R ∧ y∈R ⇒
    y≠0 ⇒
        (x/y)∈R

Here x/y is no longer forced to be a real number when y=0, indeed it is completely unconstrained.  This is obvious, isn't it?  Why then do some people find it necessary to constrain such undefined values?  Don't they realize that this unconstrainedness is necessary for composing specifications and for reducing the complexity of the rules to reason about them?

Actually the approach (3) in Abrial and Mussat is due to D. Gries, "Foundations of Calculational Logic" [in Mathematical Methods in Program Development, M. Broy and B. Schneider (Eds.), Springer, 1996].  It can also be found in C. Morgan, Programming from Specifications, Prentice Hall, 3rd Edition, 1998, section 6.7.

Kingfishers on the River Blackwater

I saw a pair of kingfishers (Alcedo atthis) this afternoon as I was walking alongside the river Blackwater between Frimley and Farnborough.  They were chasing each other up and down the river, occasionally alighting on the branches of overhanging trees, and then dashing off again, making strident cheep-cheep calls all the time.  While I have regularly seen kingfishers on this stretch of river and on the nearby lakes, this is the first time that I have ever seen two of them together.   It was also the best view I have ever had of any of these birds: before today I had only caught glimpses of a flash of blue disappearing into the distance, but this time I got a clear views as they raced past. They didn't seem to notice me.  I presume they were performing the courtship chase, mentioned in BWP-CE, though September does seem an odd time of year for courtship.  However, whatever they were doing, they certainly seemed to be enjoying themselves.

Object Identity and Time

My specification system has no built-in notion of object identity.  According to Alena Griffiths and Gordon Rose (University of Queensland SVRC Technical Report 95-38, 1995) such a system:

...has two principle defects: there is no means for distinguishing objects with identical state values, and there is no notion of object persistence.

The first of these defects does not apply to my system: If two objects have the same state values then they are the same object. Because I include the past and future in the object state, anything that can be deduced about one object can also be deduced about the other, so it doesn't matter which copy you use.

The second defect is more interesting because it reveals that object identity is closely tied to the idea of time.  Strictly speaking, if you make two observations of the same object at different times then you cannot really be sure that it is the same object.  Not only is the time property different, but also any number of other properties could also be different too (age for example).  To have a notion of persistence you have to explicitly specify a particular object identity property.  We also have to explicitly state the following constraint to ensure that each identified object has only one set of properties:

∀x. ∀y.
   objectid(x)=objectid(y) ∧ time(x)=time(y) ⇒
      x=y

With the useful half of Leibniz's definition of identity, we can conclude from the last line that all of the properties of x and y are identical.

It would be possible to chose other object identifier functions (and maybe even time functions as well), and so partition the set of objects into identity equivalence classes in different ways.  However, it is not clear to me whether this would be useful or not.

The Principles of Specification

Properties are functions on objects.  For example:

• The fields of records are property functions of those records.
• The fields and attributes of objects are property functions of those objects.
• Associations between objects are property functions of the source objects.
• Procedures and operations on objects can also be seen as property functions on those objects. This is even when they only bring about a change of state in the object, and do not appear to return any value.  In these cases it is possible to regard the next state of an object as a property of that object, and to consequently treat it as a property function.
• Time is also is also a property function of objects.  This has far-reaching implications for object identity which I shall go into in a later article on Object Identity and Time.

Any property function can be applied to any object to yield a unique value.  However, unless that property has been explicitly constrained for that class of object, we cannot deduce anything about what that unique value might be (or what its properties might be).  For example, applying the property function square to the integer 4 would yield 16, but it would also be possible to apply colour to 4 and it would yield a unique answer but, unless we had specified what the colour of that integer should be, we would not be able to deduce anything about that value; we could not even say whether it was an integer: it could be the real number pi/4, or the character string "Xy$#!", or even an object representing a bank account.

Every object has an infinite number of properties.  Two objects are identical if and only if they yield the same value for every one of these properties, even the ones that are unspecified.  In effect, this means that variables can only be identical if they refer to the same object (all their properties are the same so they are the same - this is one half of Leibniz's definition of identity: the useful half).

This object identity corresponds to reference semantics in programming languages.  It is what we get when we manipulate and copy pointers to objects rather than the objects themselves.  The pointers can be thought of as object identifiers.

The apparently more simple value semantics is actually more complicated. This is got by restricting comparisons and copying to a finite subset of properties.  For example, to compare two points on the Euclidean plane we use a function that compares only their x and y coordinates and ignores all other properties.  This form of comparison is more complicated because you need a separate special-purpose comparison function for each finite subset of properties.  For example, if we think of the above two points as being in 3-dimensional Euclidean space the function would compare the x, y and z coordinates and ignore the rest.

Chiffchaffs

On Thursday morning I got off the train at Farnborough North and was surprised to hear the alternating two-note song of a chiffchaff as I walked over the bridge. 

It was back in the spring that I first noticed one of these small, non-descript warblers belting out its distinctive song from high up on a power line, and was so intrigued that I took the trouble to look it up in BWP-CE.  It was the repetitive two-note song and the fact that it was sung from high up that convinced me that it was a chiffchaff (Phylloscopus collybita).  Over the next few weeks I would regularly hear two or even three of them each morning as I walked the half-mile through the woods to Frimley, but I never again managed to see any of them.   The song is so distinctive that I am sure that I would remember if I had heard it before, but I am fairly sure I haven't.  The two-note phrase is repeated between about five and ten times and then is followed by a lower and quieter brrr-brrr-brrr sound. 

During the summer I noticed that the chiffchaffs were no longer singing, or were only doing so much less frequently than in the spring.  Hence my surprise to hear one singing again at the start of autumn.