Undefined Values should remain Undefined

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.

Comments

[Gavin]

Quantum Computing?

Tris, have you ever had a look at Quantum Computers
and their simulation?

I'm writing a state of the art on this topic at the moment.
I'd be interested in what you make of a review paper
that is available as pdf on line:

http://rugth30.phys.rug.nl/compphys0/QCE/Doc/revqcs3.pdf

There is even a simulator program called QCE that you
can play with on Windows-XP/2K [not linux :-{].



t

[Tristram Brelstaff]

Hi Gavin,

I know nothing about quantum computing but I have had a quick look at the review paper and I reckon it would take me several years study with the open University before I could grasp most of it. The bits I could understand look interesting and, if Richard Feynman was involved in developing it then I am willing to admit that it must be worth pursuing. However, I can't help you with your paper I am afraid.

Tristram