In "On Using Conditional Definitions in Formal Theories" J. R. Abrial and L. Mussat [in D. Bert et al (Eds.), ZB2002, Lecture Notes in Computer Science. pages 242-269, Springer, 2002] review various approaches to handling undefined values. One of these, approach (3) on page 247, involves "claiming that a term of the form E/0 denotes a genuine real number, but that this number is unknown". Abrial and Mussat go on to express the opinion that it is "hard to accept" that "3/0 denotes a real number".

I agree. In my approach 3/0 denotes a value but we cannot tell what that value is, not even whether it is a real number or not: It is completely undefined. The requirement that the value must be a real number appears to arise from the inappropriate enforcement of typing requirements. The problem is that the type invariant is being (incorrectly) enforced in the post-condition, even when the pre-condition does not hold. For example, consider:

∀x,y. x∈R ∧ y∈R ⇒

(x/y)∈R

Here x/0 is required to always be in R (assuming x and y are in R), whereas what we really want is for the (x/y)∈R to be guarded as follows:

∀x,y. x∈R ∧ y∈R ⇒

y≠0 ⇒

(x/y)∈R

Here x/y is no longer forced to be a real number when y=0, indeed it is completely unconstrained. This is obvious, isn't it? Why then do some people find it necessary to constrain such undefined values? Don't they realize that this unconstrainedness is necessary for composing specifications and for reducing the complexity of the rules to reason about them?

Actually the approach (3) in Abrial and Mussat is due to D. Gries, "Foundations of Calculational Logic" [in Mathematical Methods in Program Development, M. Broy and B. Schneider (Eds.), Springer, 1996]. It can also be found in C. Morgan, Programming from Specifications, Prentice Hall, 3rd Edition, 1998, section 6.7.