There is also an interesting case of violated reflexivity in the Eiffel standard. Check ECMA-367 section 8.21.3

“The Boolean_expression e ~ f has value true if and only if the values of e and f are both attached and such that e.is_equal (f) holds.”

In other word, with x: detachable ANY, x ~ x must yield False per the Eiffel standard.

Be reassured, under Eiffelstudio it yields True.

1. I don’t have access to the standard as it seems the reference document is not free of charge. Why you must pay to know the standard is one topic but I’ll leave it for another time. Wikipedia has a link to a recent draft (1.2.9) and I believe you’re refering to section 7.11 that I will quote here:

“Comparisons are exact and never overflow or underflow. Four mutually exclusive relations are possible: less
than, equal, greater than, and unordered. The last case arises when at least one operand is NaN. Every NaN
shall compare unordered with everything, including itself. Comparisons shall ignore the sign of zero
(so +0 = −0). Infinite operands of the same sign shall compare equal.

Languages define how the result of a comparison shall be delivered, in one of two ways: either as a condition
code identifying one of the four relations listed above, or as a true-false response to a predicate that names the
specific comparison desired.”

I didn’t see anything else in this draft specifying that NaN comparison should yield false, however “Every NaN
shall compare unordered with everything, including itself” leaves no doubt about that since unordered is not equal.

Note that raising an exception would violate the standard, I believe, since comparing two numbers even if one is a NaN is a non-signaling operation.

2. I think the problem is that we want to maintain not two properties (equality is reflexive, and NaN /= NaN) but three, the third being that all objects can be compared. This is captured by the fact that is_equal is a feature of ANY, while other comparison features such as is_less come from specialized classes like COMPARABLE.

In a world with is_equal being a feature of an abstract class (EQUATABLE? It sounds ugly) the REAL class would not inherit this feature. Real numbers could not be compared with is_equal. They would be compared with a dedicated feature taking one of “less than”, “equal”, “greater than” and “unordered” as an argument, that could then safely return true or false as specified by the standard.

3. I’ve been confronted in the past with problems such as this one. Almost always, it comes from trying to mix orange and apples in a single value or concept. The way out is then to clearly separate the involved values and concepts in different entities. For instance, consider this definition of REAL:

class REAL
…
feature
value: ARRAY[INTEGER_8] — The numeric value
meaningful: BOOLEAN — False if a NaN
…
end

Then the value of a number is separate from the boolean attribute that indicates if it has a meaning. The proper redefinition of is_equal becomes

is_equal (other: like Current): BOOLEAN
do
if meaningful and other.meaningful then
result := value.is_equal(other.value)
else
result := False
end
end

This definition satisfies x /= x when x.meaningful is False.

4. You could argue that this is only an artificial trick to reconcile Eiffel contracts and the IEEE standard. I think it goes deeper than that. Equality in Eiffel, and probably all languages, is only an approximation of mathematical equality. If you asked, during a math course “does x = x?” then sure I’d answer yes. But during a computing course? I’d answer “depends…”. Many aspects of computer languages are traductions of mathematical operations and properties that want to stay as close as the original concept, but never succeed that it.

There are well known examples. Take this function for instance:

identity_with_a_trick (n: INTEGER): INTEGER
do
result := n * 2
result := result // 2
ensure
same_value: result = n
end

It is naive to think that dividing or multiplying a number is harmless, it can raise an exception. The function above can raise a post-condition violation exception.

So to answer prof. Meyer’s question “A programming language should support the venerable properties that equality is reflexive and that assignment yields equality (…) Do you agree?” I respectfully disagree in general, and fully agree when equality is defined for the objects being compared. IEEE 754 standard simply states it isn’t.

If a1, a2, … and b1, b2, … are sequences of real numbers that both approach 0, then the sequence of quotients a1/b1, a2/b2, … in general will not approach any real number, but will rather have a set of (extended) real numbers as its limit (the smallest of which is known as the inferior limit and the largest of which is known as the superior limit).

We can adopt the convention that an ordinary function applied to a set is equal to the set of function values, and we can then go on to calculate with sets of real numbers much as with real numbers (the first person to do this may have been Weierstrass). Let us now consider the question of equality between such sets. We know that {3, 4} and {4, 7} are different by ordinary set equality, but if we apply the equality function to the pairs (3, 4), (3, 7), (4, 4), and (4, 7) then the results will be False, False, True, and False, respectively, giving us the set {False, True}. In fact, we get the same result if we compare {3, 4} to itself.

How are we to interpret an equality that evaluates to {False, True}? If we interpret it as True then transitivity of equality will quickly lead to all real numbers allegedly being one and the same thing. I would say that what this really means is that there is a not-too-unnatural sense in which all real numbers are _equivalent_. If we interpret {False, True} as being False, then we allegedly have things/objects/entities which are not equal to themselves (or maybe I should say that we have a single thing/object/entity which is not equal to itself – without equality we have no standard for counting things.). Finally, we may prefer to restrict the domain of definition of our equality relation so that the cases that gave {False, True} are excluded from consideration.

Based on these three possibilities one might conclude that we cannot have NaN=NaN without getting x=y for any real numbers x and y (thus vindicating IEEE 754). However, we also have the set equality that makes {3, 4} distinct from {4, 7}, and we can use this type of equality to introduce yet another type of equality: We may consider all sets that contain more than one real number to be one and the same object, and we may call this object “NaN”. In fact, there is mathematical research that supports treating NaN as a first-class object: See http://en.wikipedia.org/wiki/Wheel_theory .

Math is partial and there are different ways to handle this. Problems show when these ways are mixed, for example through the interactions between Boolean and Real.

One way is the use of NaN and any other 3-valued logic. But then, Boolean value should have a NaB. Another is the use of preconditions. That is what Eiffel uses. To be consistent, Eiffel should raise a precondition violation whenever an operation would produce a NaN.

Of course, floating-point numbers are imperfect substitutes for mathematical real-valued numbers – I think REAL is a poor choice of name for the type in a programming language, as it has the potential to mislead the mathematically minded – since many functions on floating-point values that a mathematician would expect to be identity functions will turn out to accumulate imprecision, resulting in similarly surprising x != x.

Kind regards,

Ian

In void-safe mode the compiler will reject the code (although I haven’t checked this yet on an actual example).

across s as c loop print (c.item) end

If ’s’ is declared to be of a detachable type, and if it actually is Void at run time, does this ‘across’ loop raise a Void-target call exception? (This is what C# does if the structure supplied to a ‘foreach’ loop is null. I’m fixing one such NullReferenceException bug right now that has gone undetected for months in our C# code.) Or does ‘across’ recognise that the structure is Void, and treat it the same as if it were empty, performing zero iterations of the loop? (This is what I wish C# ‘foreach’ loops did; I wish it frequently, unfortunately.)

Or would the Void-safe Eiffel compiler reject the above code if ’s’ is detachable?

- The simplest is to make the class a descendant of one of the existing descendants of the ITERABLE class, such as INDEXABLE (which is for example used as ancestor by all the list classes). Then you have nothing more to do; you get a standard cursor.

- If you want a more specific cursor, make the class a descendant of ITERABLE and write the specific cursor class as a descendant of ITERATION_CURSOR, effecting the queries `item’ and `off’. This gives you finer control in case your structure has specific properties that should be accessible through the cursor. As an example, you can look at how this was done for HASH_TABLE in such a way that in a loop

across my_hash_table as mht loop … end

you can in a loop body access both mht.item, giving the current item in the hash table, and mht.key, giving its key.

I will release my current implementation as open source in a few weeks.

the calculus is very exciting. I’d be really interested in analyzing some larger code (e.g. different algorithms).
My questions:
- how does the calculus cope with virtual method calls? The paper says that the concepts of inheritance and genericity have only a marginal effect on aliasing, but it seems to me that you have to take into account the actual type of the object.
- do you have any open-source implementation of your analyzer? (Probably I need to implement my own, but having some working example would be very helpful.)

Thanks,
Mate

Even without dynamic binding, however, it is important to realize that aliasing is fundamentally non-compositional. as demonstrated at the beginning of section 3.4. The closest to a compositionality rule is the qualified call rule (/36/), which shows the dependence and influence on the environment.

It would be nice to be able to define the “alias relation induced by a routine r”, say a (r), then, if a larger environment e includes calls to r, to define a (e) as a function of a (r) and a (x) for other components of e. Unfortunately that is not possible. As the paper shows, we can only defined the alias relation induced by r ___in reference to the alias relation that holds for a particular call to r___ (using the qualified call rule).

More precisely, if r always creates an aliasing between x and y, then any environment including calls to r may cause that aliasing. But the reverse property does not hold: if examination of r alone does not lead to identifying an aliasing between x and y, we can deduce no general property from this observation; a call could result in x and y becoming aliased. For example x and y could be respectively aliased to different formal arguments of r, and then a particular call might use actual arguments that are aliased to each other.

In fact, Mr. Brandl’s post provides an excellent informal example of this. Looking at the present blog (in its state as I write this message), we can deduce that he did not make any comment related to a comment by Jules Jacobs. Now it turns out that Mr. Brandl posted his comment, identically, on both this blog and the “Lambda the Ultimate” blog. If I mention here that “comments #1 and #13 on the first external blog referring to this topic are related” I introduce an aliasing of sorts between the two authors, which is only visible when we consider the two blogs together.

We have to reconcile ourselves with the realization that aliasing has some inevitably global aspects. Of course I agree with both comment authors that it is very desirable to make the solution as modular as possible for the programmers and appreciate the challenge to do so.

I like the fact, that no new notation is necessary in the program text. This is an advantage over dynamic frame contracts.

You build the alias relation bottom up, starting from elementary statements (i.e. the effect of the statements on the alias relation) to more complex statements.

But this might be also one of the weak points to solve the framing problem for OO Software. As far as I have understood your theory, it does (in its current state) not go well with dynamic binding and modular reasoning. Consider a parent class which introduces some deferred features (i.e. features with contracts only). A client using these features does not see the implementation.

How can you calculate the effect of a call to a deferred routine on the alias relation? If you do dynamic typeset calculation you can calculate the union of all effects. But then you leave modular reasoning. If you want to stick to modular reasoning, you certainly have to introduce some notation for deferred features to specify the effect on the alias relation which is binding for the descendants (like Bernd Schoeller did for his frame contracts).

I first thought you were referring to the loop invariant, but it is correct — it mentions fibonacci (i-1), which is always defined, not fibonacci1. Of course it would make no sense for a loop invariant to use the enclosing function.

Second, thanks for the link to the sample chapter on recursion. I’m looking forward to studying it in detail.

Third, as someone who doesn’t even qualify as a beginner in Eiffel, I was surprised by the statement on page 440 (of the sample chapter) that “The following function indeed yields the same result…” in one case. Is fibonacci1(0) actually allowed, given the requirement (n >= 1)? Or is the problem my own ignorance of the meaning/usage of “require positive: n >= 1″?

Andrea

Asking wikipedia for the existance of such a clock, I found out about the astronomical clock in which the Zodiac signs are moving counter clockwise. I guess that could be it.

There seem to be a number of solutions… But interesting problem.

When will you post a solution?

This post was mentioned on Reddit by doomglobe: They were on opposite ends of adjoining city blocks? I didn’t know iphones had service in prague! This story is a lie! They both had blackberries!…