Undefined expressions and logic in Z and B
In this paper we show how undefined expressions and undetermined predicates may arise when using the specification languages Z and B. We review how undefined terms have been handled in various formalisms (Principia Mathematica, Domain Theory, LPF,) and look at the effect of undefined expressions on the proof theory and the denotational meaning of specifications in Z and B. We note that in formal systems which make use of partial functions and have an unguarded equality axiom x = x together with a classical two valued logic it is impossible to have a proof rules of the form y = f(x) --> x bar right arrow y is an element of f and that consequently, assertions of the form y = f(x) may have very little meaning.
undefined expressions z b denotational semantics theory of descriptions