SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

An Introduction to Formal Specification and Verification Using EHDM
 by Sam Owre, Dr. John Rushby & Friedrich von Henke.

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 pro gram 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.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy