Skip to main content
SpringerLink
Log in

Z User Workshop, York 1991

Proceedings of the Sixth Annual Z User Meeting, York 16–17 December 1991

  • Conference proceedings
  • © 1992

Overview

Editors:
  1. J. E. Nicholls

    1. Programming Research Group, Oxford University Computing Laboratory, Oxford, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Workshops in Computing (WORKSHOPS COMP.)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (17 papers)

  1. Front Matter

    Pages i-viii
    Download chapter PDF

  2. Theoretical Foundations

    1. Front Matter

      Pages 1-1
      Download chapter PDF

    2. On Recursive Free Types in Z

      • Alf Smith
      Pages 3-39

    3. On Free Type Definitions in Z

      • R. D. Arthan
      Pages 40-58

    4. Z and Hoare Logics

      • Antoni Diller
      Pages 59-76

    5. W: A Logic for Z

      • J. C. P. Woodcock, S. M. Brien
      Pages 77-96

  3. Scope of Use

    1. Front Matter

      Pages 97-97
      Download chapter PDF

    2. The use of Z

      • Rosalind Barden, Susan Stepney, David Cooper
      Pages 99-124

    3. Extending the Useful Application Domain for Formal Methods

      • Paul A. Swatman, Danielle Fowler, C. Y. Michael Gan
      Pages 125-144

    4. Domains of application for formal methods

      • J. E. Nicholls
      Pages 145-156

    5. Z—, an Executable Subset of Z

      • Samuel H. Valentine
      Pages 157-187

  4. Special Applications

    1. Front Matter

      Pages 189-189
      Download chapter PDF

    2. Engineering Human-Error Tolerant Software

      • Michael Harrison
      Pages 191-204

    3. Techniques for Partial Specification and Specification of Switching Systems

      • Pamela Zave, Michael Jackson
      Pages 205-219

  5. Tools

    1. Front Matter

      Pages 221-221
      Download chapter PDF

    2. Z and Eves

      • Mark Saaltink
      Pages 223-242

    3. zed B: A Proof tool for Z built on B

      • Dave Neilson, Divya Prasad
      Pages 243-258

  6. Structured Methods and Object-Oriented Approaches

    1. Front Matter

      Pages 259-259
      Download chapter PDF

    2. A Method for the Specification of Relational Database Applications

      • Roberto S. M. de Barros, David J. Harper
      Pages 261-286

    3. Structured Analysis — A Draft Method for Writing Z Specifications

      • Fiona Polack, Mark Whiston, Peter Hitchcock
      Pages 287-328
Back to top

Keywords

About this book

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.

Editors and Affiliations

  • Programming Research Group, Oxford University Computing Laboratory, Oxford, UK

    J. E. Nicholls

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation