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.

Invariants should be Unadorned

Properties that always hold, ie: invariants, should not have to be indicated by special notations.  They should be unadorned.  Special notations should only be used to indicate when a property does not always hold.

Lamport's Temporal Logic of Actions violates this principle in that a predicate P holds only in the initial state, and if you want to indicate that it always holds the you have to put a box symbol in front of it:

[]P

Similarly, in Daniel Jackson's Micromodularity Mechanism you have to use the keyword 'fact' to indicate that a predicate is invariant.

It seems obvious and natural to me that if a predicate P does not always hold then this should be indicated by an implication Q->P where Q is the condition under which P does hold. 

Specifications are for Reasoning From

We write specifications of systems in order to be able to reason about those systems.  This reasoning can be formal or informal. It can take the form of proving properties, deriving properties or refining the specification to code.  The purpose of specifications is to allow this reasoning to take place, ie: specifications are for reasoning from.  Looking at specification this way leads me to make the following suggestions:

• Specifications should be written in a way that makes reasoning easy.  A way to do this is to write them as conjunctions of ready-to-use proof steps, with the pre-conditions and variables of each step clearly visible.
• Conciseness is not necessarily important in specifications.  Not including irrelevant material is important, as is clearly laying out the relevant material, but using abstruse theories to make the specification as short as possible is not.
  
• Graphical notations that have not been designed with reasoning in mind should be avoided.  Just because a notation is graphical does not mean that it makes reasoning easy.
  

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.