An Introduction to Formal Specification and
Verification Using EHDM
John Rushby, Friedrich von Henke, and Sam Owre
CSL Technical Report SRI-CSL-91-2
Abstract
This report is a tutorial on formal specification and verification
using Ehdm. The Ehdm specification language is very expressive, based
on a strongly-typed higher-order logic, enriched with elements of the
Hoare (relational) calculus. The type system provides subtypes,
dependent types, and certain forms of type-polymorphism. Modules are
used to structure large specifications and support hierarchical
development. The language has a complete formal semantic
characterization and is supported by a fully mechanized specification
and verification environment that has been used to develop large
specifications and perform very hard formal verifications.
The tutorial uses simple examples to describe the Ehdm language,
methodology, and tools. The first examples illustrate the basic ideas
of specification and theorem proving in Ehdm. We then introduce the
ideas of testing specifications, of horizontal and vertical hierarchy,
and of consistency and conservative extension. Later chapters cover
more advanced topics including subtypes, higher-order logic, proofs by
induction, and program verification using Hoare logic. The tutorial is
illustrated throughout with self-contained examples of Ehdm
specifications and proofs, all of which have been mechanically
checked.
Paper
PDF
BibTeX Entry
TBD
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page