| Z User Workshop, York 1991: Proceedings of the Sixth Annual Z User Meeting, York 16-17 December 1991 Softcover Repri Edition Contributor(s): Nicholls, J. E. (Editor) |
|
 |
ISBN: 354019780X ISBN-13: 9783540197805 Publisher: Springer OUR PRICE: $52.24 Product Type: Paperback Published: August 1992 |
| Additional Information |
| BISAC Categories: - Computers | Software Development & Engineering - General - Computers | Compilers - Computers | Logic Design |
| Dewey: 005.133 |
| Series: Workshops in Computing |
| Physical Information: 0.85" H x 6.69" W x 9.61" (1.45 lbs) 408 pages |
| Descriptions, Reviews, Etc. |
| Publisher Description: In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z 3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1 The following Z specification of a functionf, from integers to integers "f x: 1 x O- fx = x + 1 (i) "f x: 1 x O- fx = x + 2 (ii) is inconsistent, because axiom (i) gives f 0 = 1, while axiom (ii) gives f 0 = 2. This contradicts the fact that f was declared as a function, that is, f must have a unique result when applied to an argument. Hence no suchfexists. Furthermore, iff 0 = 1 andfO = 2 then 1 = 2 can be deduced From 1 = 2 anything can be deduced, thus showing the danger of an inconsistent specification. Note that all examples and proofs start with the word Example or Proof and end with the symbol.1. |