Golden Pheasant

On Friday afternoon my wife Liz, her sisters, and my daughter Zoe saw a male golden pheasant (Chrysolophus pictus) in the grounds of Reading University.  It was being slowly shooed down the drive from Foxhill House by the driver of a van.  Apparently it had escaped from a nearby garden where it was being kept as a pet.  These spectacular birds are native to central China but were introduced to Britain as an ornamental bird for aviaries and parkland.  I was still on my way home from work and so missed all the fun. 


Kingfishers Again

Last week I saw at least one of the kingfishers more or less each day as I was walking to and from the station, alongside the Blackwater.  On one occasion I came across one one of them perched still on a branch over the river.  It stayed for about ten seconds, allowing me to get a good view of its plumage, then it flew off.  It was tiny: little bigger than a robin.

On Sunday I took Zoe to see them but there was no sign of them.  Maybe that was because there were too many people around, it being the middle of the day.  Next time I will take her in the early morning. 

Today, I saw one of them again, in the morning and in the afternoon.


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

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 ⇒

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) ⇒

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.