Skip to main content
SpringerLink
Log in
Book cover
  • Textbook
  • © 1994

Proof in VDM: A Practitioner’s Guide

Authors:

  1. Juan C. Bicarregui
    View author publications

    You can also search for this author in PubMed   Google Scholar

  2. John Fitzgerald

    1. University of Newcastle upon Tyne Dept. Computing Science, Newcastle upon Tyne, United Kingdom

    View author publications

    You can also search for this author in PubMed   Google Scholar

  3. Peter A. Lindsay
    View author publications

    You can also search for this author in PubMed   Google Scholar

  4. Richard Moore
    View author publications

    You can also search for this author in PubMed   Google Scholar

  5. Brian Ritchie
    View author publications

    You can also search for this author in PubMed   Google Scholar

Part of the book series: Formal Approaches to Computing and Information Technology (FACIT) (FACIT)

Buy it now

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

About this book

Formal specifications were first used in the description of program­ ming languages because of the central role that languages and their compilers play in causing a machine to perform the computations required by a programmer. In a relatively short time, specification notations have found their place in industry and are used for the description of a wide variety of software and hardware systems. A formal method - like VDM - must offer a mathematically-based specification language. On this language rests the other key element of the formal method: the ability to reason about a specification. Proofs can be empioyed in reasoning about the potential behaviour of a system and in the process of showing that the design satisfies the specification. The existence of a formal specification is a prerequisite for the use of proofs; but this prerequisite is not in itself sufficient. Both proofs and programs are large formal texts. Would-be proofs may therefore contain errors in the same way as code. During the difficult but inevitable process of revising specifications and devel­ opments, ensuring consistency is a major challenge. It is therefore evident that another requirement - for the successful use of proof techniques in the development of systems from formal descriptions - is the availability of software tools which support the manipu­ lation of large bodies of formulae and help the user in the design of the proofs themselves.
Back to top

Authors and Affiliations

  • University of Newcastle upon Tyne Dept. Computing Science, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

Back to top

Bibliographic Information

  • Book Title: Proof in VDM: A Practitioner’s Guide

  • Authors: Juan C. Bicarregui, John Fitzgerald, Peter A. Lindsay, Richard Moore, Brian Ritchie

  • Series Title: Formal Approaches to Computing and Information Technology (FACIT)

  • Publisher: Springer London

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag London Limited 1994

  • Softcover ISBN: 978-3-540-19813-0Published: 01 December 1993

  • Edition Number: 1

  • Number of Pages: XVI, 362

Back to top

Publish with us

Policies and ethics

Back to top

Buy it now

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

Search

Navigation