文档介绍：1. Introduction
Logic is the study of the relation between a symbolic
language and its meaning, with special emphasis on the
legitimate ways of reasoning in the language. A primary
Programming Techniques M. Douglas Mcllroy* plishment of mathematical logic in the earlier part
and Data Structures Editor of this century was the formalization of the first-order
predicate calculus, a logical language that is generally
A Critique of the Foundations regarded as sufficient in principle for nearly all mathe-
of Hoare Style Programming matical discourse. Formal rules for reasoning in the first-
order predicate calculus have been shown to be correct
Logics and powerful enough to derive all true theorems of this
language. In the last decade, new languages and formal
Michael J. O'Donnell
rules for reasoning about programs have been proposed
Purdue University
and attempts have been made to justify the correctness
of these rules.
A particularly popular language for reasoning about
Much recent discussion puting journals has programs is the language of Hoare triples [15]. The
been devoted to arguments about the feasibility and Hoare language includes the formulas of the first-order
usefulness of formal verification methods. Too little at- predicate calculus plus triples of the form A {P}B, with
tention has been given to precise criticism of s