Towards a Calculus of Object Programs
I posted here a draft of a new article, Towards a Calculus of Object Programs.
Here is the abstract:
Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here, a Calculus of Object Programs, combines four components: compositional logic, a framework for describing program semantics and proving program properties; negative variables to address the specifics of O-O programming, in particular qualified calls; the alias calculus, which determines whether reference expressions can ever have the same value; and the calculus of object structures, a specification technique for the structures that arise during the execution of an object-oriented program.
The article illustrates the Calculus by proving the standard algorithm for reversing a linked list.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy
I wish I had your writing skills. Well written article, thanks.
I would like to add some comments.
1. Compositional calculus
Your axiom AX/5 (x:=e); x = e is not true generally. Counterexample: “(x:=”Hello “+”world!”);x /= “Hello “+”world!”. It is only valid if `e’ is a referentially transparent expression (condition AX/5 can be used to define referentially transparent expressions).
Your presented proof on list reversal is not affected by this shortcoming, because it uses only referentially transparent expressions.
I cannot say if this bug can be fixed easily in the compositional calculus. Since your reasoning require this “axiom” heavily it might require considerable rework.
2. Abstraction
In your paper you don’t talk about queries, you use attributes. This is the implementation view. You use a class LINKABLE with features “right” and command “put_right”. The client should not rely on the fact that “right” is an attribute. The client should rely only on the properties of the query “right”. In case of an attribute it is evident that an expression “cell.right” is referentially transparent, in case of a query this is not evident. Therefore I fear that your presented theory has the same problem as already discussed after your published your “alias calculus”. It does not support local reasoning for lack of abstraction.
Helmut
Thanks for the comments.
On point 1, the article states (end of 2.3, page 6) that equality represents object equality.
On point 2, you are right that the discussion should be generalized to queries; indeed there is little that is specific to attributes.
Point 1: Nice try. But it does not help. You just have to dig one level deeper to uncover the problem: x:=[“Hello”, “world”]; x /= [“Hello”, “world”], even if “=” represents object equality.
Object equality can (and often is) redefined for every specific class. The redefinition for pairs should make it clear that pairs are equal iff their respective elements are equal.
Then you dig just one level deeper and the same problem arises.
Or do you want to say that “=” always means deep equality?
Does your theory depend on the user redefining object equality properly to fit your axiom?
Not deep equality, just plain equality as adapted to every object type (as for example to container classes in EiffelBase). Redefine is_equal.
If “=” means plain object equality, then my original comment “Your axiom AX/5 (x:=e); x = e is not true generally” is still valid. It is easy to construct a type T and an expression e of type T, where
– e creates some attributes of the returned object (or subattributes or subsubattributes)
– and is_equal requires the attributes to be identical in order to return true.
To the best of my knowledge there is no rule with prevents me from doing that. Maybe you have such a rule in mind.
Reference case: reference equality implies object equality.
Expanded case: assignment causes a copy; `copy’ has `is_equal’ in its postcondition.
From our previous discussion I conclude that I have not yet made my point sufficiently clear. Since the point is subtle, it might require more explanation.
In your object calculus you stated the axiom
(x:=e); x = e (AX/5)
i.e. after the assignment “x:=e” evaluating “x” yields the same as evaluating “e” in the context before the assignment (“e” is an arbitrary expression). On the surface this axiom is true because of the obvious fact that if you assign something to a variable, the variable will “be equal” to the expression which is assigned to it after the assignment.
Assuming the current semantics of “=” in Eiffel, which is reference equality for reference type objects and object equality for expanded type objects the “problem” of AX/5 is not very difficult to see. Any expression returning a newly created object invalidates it. In my first example I have used manifest strings which implicitely create new objects. The counter example is very simple
(x:=”any string”); x = “any string” — invalid!
is not true, because the two invocations of “any string” create two individual strings, each having an own reference. The two references are definitely different.
This shortcoming of my simple counter example can be remedied by assuming object equality for “=”, because the two invocations of “any string” yield equal strings. So let us assume “=” expresses object equality (i.e. interpret it as “~” of ECMA Eiffel which is based in “is_equal” and not on “is_deep_equal”).
In that case one has to dig deeper to uncover the problem. Since “=” now means object equality, we need a different operator to express reference equality. In the sequel I use “==” to express reference equality (I assume that you keep a notion of reference equality in Eiffel).
class T inherit ANY redefine default_create, is_equal feature
s:STRING
default_create do s:=”any string” end
is_equal(o:like Current): BOOLEAN do Result := (s == o.s) end
end
Note that two different objects of type T can never be equal with respect to object equality!
Now it is easy to construct the counter example:
(x:= create T); x = create T — invalid!
is not valid. The only escape would be to assign to “=” the semantics of deep equality. But you claimed that plain equality is sufficient.
To recapitulate:
In AX/5 “(x:=e); x = e” the problem is not the assignment. The assigment by itself is pure. It doesn’t modify anything except the contents of the variable (local or attribute) assigned to. The problem is the expression. As soon as object creation in an expression is involved the assertion
e = e — not valid in general!
is not longer true in general. Different invocations can create different objects with different attributes etc. That is the reason why you cannot do weakest precondition calculus in its classical form with object oriented SW. The corresponding axiom to AX/5, the so called assignment axiom
wp(“x:=e”,R) = R[x:=e]
where “R[x:=e]” means textual substitution of all occurrences of “x” by the expression “e” requires referential transparency of expressions which is not given for expressions involving object creations.
Another axiom which is not valid in general:
On page 12 you state
i; Current = Current — for any instruction i CUR/4
with the explanation that no statement can change the value of Current. CUR/4 is obviously true for objects of reference type with “=” expressing reference equality.
Now what happens if Current refers to an expanded type and “i” is an instruction which changes an attribute of that expanded type object. Unless you assume immutability for expanded type objects CUR/4 is already invalid for expanded type objects, since “=” means object equality for expanded type objects.
But since you explained that “=” must be interpreted as object equality in general CUR/4 is not even valid for reference type objects. Any unqualified command might change the content of the current object which is therefore no longer equal (object equality) to its state before the command.