Definitions and Designations

The following is from J. R. Abrial and L. Mussat  ["On Using Conditional Definitions in Formal Theories",  in D. Bert et al (Eds.), ZB2002, Lecture Notes in Computer Science. pages 242-269, Springer, 2002]:

Suppes first introduces two criteria characterizing the definition of new symbols in a formal theory: (1) the Criterion of Eliminability, and (2) the Criterion of Non-creativity. The former requires that "any definition introducing a new symbol may be used to eliminate all subsequent meaningful occurrences (of that new symbol)". The latter requires that any definition of a new symbol "(does not) make possible the derivation of some previously unprovable theorem stated wholly in terms of primitive and previously defined symbols". In other words, a proper definition must not add any extra "power" to a theory, it is just a useful, but not indispensable, extension to it.

This means that definitions are just abbreviations and therefore cannot be used to build a theory; they can only be used to express an existing theory in a different way.

Michael Jackson ["Software Requirements and Specifications", Addison Wesley, 1995, pages 51-54] has some interesting things to say on the subject of the symbols used in specifications:

One way to define a term is to give a designation. That means giving a recognition rule for recognizing some class of phenomenon that you could observe in a domain. In the domain of human relationships you might have these designations:

x is a human being (homo sapiens) = Human(x)

x is male = Male(x)

x is female = Female(x)

x is the biological (genetic) mother of y = Mother(x,y)

x is the biological (genetic) father of y = Father(x,y)

[...] You can use the designated terms in refutable descriptions that make assertions about the domain. [...]

Thus designated terms (symbols) here connect the theory with the domain that the theory describes. Jackson goes on:

Now suppose that you want to make some assertions about grandparents, and aunts and uncles, and cousins and brothers and sisters.  You don't have any designations for these terms, but it will be very inconvenient and difficult to do without them.  there are two ways of making them available for use in your descriptions.  One way is to write some more designations.  For example

x is the genetic full brother of y = Brother(x,y)

[...]

Sometimes this is the right thing  to do.  But probably it is not the right thing here.  The right thing here is to do it the other way: to give a formal definition of each of the new terms, using the terms you have already designated.  [...]

Brother(x,y)  ≙ 
  Male(x) ∧
     ∃ f . (Father(f,x) ∧ Father(f,y) ) ∧
     ∃ m . (Mother(m,x) ∧ Mother(m,y) )

This is a definition in the style of Suppes.   However, I think it is unsatisfactory to regard 'Brother' as purely a convenience to make the theory shorter.  If it was, then it wouldn't matter if you replaced 'Brother' by say 'Aunt' throughout the theory.  The choice of names is important even in strictly unnecessary definitions.  They also designate things in the domain.

In my way of specifying there is no need to introduce new symbols, as all possible symbols already exist.  Writing a specification is just a matter of defining the constraints on these already existing symbols.

(By the way, did you spot that the definition of Brother requires the extra constraint x ≠ y?  Without this I would be my own brother.)

Eric Hehner on Model-Checking

A year or so ago I came across the following passage which nicely highlights the limitations of using model-checking to verify that programs meet their specifications:

There is an approach to program proving that exhaustively tests all inputs, called model-checking. Its advantage over the theory in this book is that it is fully automated. With a clever representation of boolean expressions (see Exercise 6), model-checking currently boasts that it can explore up to about 10^60 states. That is more than the estimated number of atoms in the universe! It is an impressive number until we realize that 10^60 is about 2^200, which means we are talking about 200 bits. That is the state space of six 32-bit variables. To use model-checking on any program with more than six variables requires abstraction; each abstraction requires proof that it preserves the properties of interest, and these proofs are not automatic. To be practical, model-checking must be joined with other methods of proving, such as those in this book. (Eric C. R. Hehner, A Practical Theory of Programming, 2nd ed, 2002)

Incidentally, you can find an online copy of Hehner's ground-breaking book at http://www.cs.toronto.edu/~hehner/aPToP/.  Unfortunately, many people have not yet noticed that the ground has been broken and seem to be busy trampling it flat again!

Eiffel and 'Design by Contract'

Tony Hoare famously wrote of the programming language ALGOL 60 that it was "so far ahead of its time  that it was not only an improvement on its predecessors but also on nearly all its successors".  In a way, the same could also be said of Eiffel, a pure object-oriented programming language designed by Bertrand Meyer in 1985.  The key to Eiffel's superiority over "nearly all of its successors" is the idea of 'design by contract' (DBC). This idea provides key insights into many areas of programming and programming language design, and Meyer has used it to produce clean solutions to problems which have given rise to unnecessarily complex messes in other languages. The best exposition of 'Design by Contract' remains Meyer's book 'Object Oriented Software Construction' (2nd Edition) but Eiffel Software (the company founded by Meyer) also have some nice Macromedia Flash introductions to Eiffel and Design by Contract at http://www.eiffel.com/developers/presentations/.

Bertrand Meyer's Word Games in OOSC2

In his magnum opus, Object Oriented Software Construction (2nd Edition), Bertrand Meyer refrains from explicitly mentioning 'Eiffel', the name of the programming language he is expounding, until the very end of the Epilogue.  However, it is fairly well known within the Eiffel community that 'EIFFEL' is encoded in the first letters of the text of chapters 1 to 6.  Well, that is not the end of Meyer's word games.  After a little research, I have discovered the following:

The first letters of each of the 36 chapters are, in order:

EIFFELEIFFELEIFFELEIFFELEIFFELEEIFEL

That is, five EIFFEL's followed by an EEIFEL.  Presumably chapters 32-33 have been changed since the first edition.  Maybe someone could check this out for me?

Following chapter 36 there is a two-page epilogue entitled:

Epilogue, In Full Frankness Exposing the Language

The first letters of this, ignoring the 'the', spell out EIFFEL.

The epilogue also consists of six paragraphs, the first letters of which spell out (yes you've guessed it) EIFFEL.

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.