Specifying the Semantics of While-Programs: A Tutorial and Critique of a Paper by Hoare and Lauer,

Abstract

Three kinds of mathematical objects are considered which can be designated as the 'meaning or 'semantics' of programs: binary relations between initial and final states, binary relations on predicates (partial correctness semantics), and functionals from predicates to predicates (predicate transformers). We exhibit various formal specification mechanisms: induction on program syntax, axioms, and deductive systems. We show that each kind of semantics can be specified by several different mechanisms. As long as arbitrary predicates on states are permitted, each kind of semantics uniquely determines the others -- with the sole exception of the weakest pre-condition semantics for nondeterministic programs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1979
Accession Number
ADA068967

Entities

People

  • Albert R. Meyer
  • Irene Grief

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Consistency
  • Department Of Defense
  • Instructions
  • Language
  • Massachusetts
  • Military Research
  • New York
  • Notation
  • Programming Languages
  • Relational Database Management Systems
  • Specifications
  • Standards
  • Structured Programming

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.