A Proof Rule for Euclid Procedures.

Abstract

The proof rules of Euclid, like the axiomatization of Pascal, presents a single definition of the various features of the language being defined. Little effort is made to explain the proof rules or to compare them to alternatives. In this paper we take one of our more complex proof rules, the rule for procedure definition and call, and attempt both to explain its workings and to compare it to two alternative rules. The rules we have chosen for comparison are Hoare's adaptation rule, from which our rule is derived, and the Pascal procedure-call rule. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 23, 1977
Accession Number
ADA041625

Entities

People

  • James J. Horning
  • John V. Guttag
  • Ralph L. London

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • California
  • Canada
  • Classification
  • Computational Science
  • Computer Programming
  • Information Science
  • Language
  • New Brunswick
  • Notation
  • Programming Languages
  • Security
  • Universities
  • Verification

Readers

  • Computational Linguistics