Thanks for the reference.

While what is not broken does not require fixing, what is broken does. My father used to say, “If it hurts, don’t do it.” At 48, I feel a little liberty to now add a little to his statement:

“If it hurts, don’t do it. If you don’t know why, find out.”

Have the courage to BE CURIOUS!

(Thanks Dad!)

Regarding the bytypalism: I am a native Russian speaking SW engineer living abroad, and I can quickly touch-type on both Cyrillic and English International keyboards (these two layouts I always have installed on the PC where I happen work, plus some handy key to switch between them in one touch – on my Linux-driven Dell laptop it’s currently a Windows key ). Funny is that even though I can touch-type, I would not be able to draw either English or Russian keyboard layout from my head

In the Natural Sciences people experiment and compare with theory and reproduction of results rather than opinion is essential. The boorishness of comment is thus reduced although jealousy and ambition is detectable.

I am aware that for some in CS, application to solving problems in the natural world is not seen as quite so respectable. However for myself working for many years in pattern recognition it has been a real joy, although I have not as a result published in CS and not been subject to the negativity articulated in this article!

———————————
Bertrand,

If testing is the only defect removal activity without prior inspections or static analysis, you will find many bugs but quality will be poor. Testing alone seldom tops 85% in cumulative defect removal efficiency so 15% of your bugs will be delivered to clients.

If you do inspections and static analysis prior to testing, you will find very few bugs during testing because most were already eliminated. Your cumulative defect removal efficiency will be above 95% and possibly approach 99%.

I sent some spreadsheets that show the differences between high quality and low quality. If others want to see them send an email to capers.jones3@gmail.com with a valid return.

Most forms of testing only find about 35% or one bug out of three. You need 8 to 12 test stages at that low level of efficiency. Inspections and static analysis, on the other hand, run from 65% to more than 85% in defect removal efficiency.

Regards,
Capers Jones
———————

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.

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.

- 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.