« Kingfishers on the River Blackwater | Main | The Principles of Specification »

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.


Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.
Author Email (optional):
Author URL (optional):
All HTML will be escaped. Hyperlinks will be created for URLs automatically.