Can I read Program Specifications and Their Proofs on EtoBox?

Program Specifications and Their Proofs is a book available to read on EtoBox.

What is Program Specifications and Their Proofs about?

In this chapter, we will explore methods of specifying programs in the simple imperative language and of proving such specifications formally. We will consider both partial correctness, where one specifies that a program will behave properly if it terminates, and total correctness, where one also specifies that a program will terminate. For partial correctness we will use the form of specification invented by C. A. R. Hoare, while for total correctness we will use an analogous form based on the ideas of E. W. Dijkstra. At the outset, it should be stressed that formal proofs are quite different than the traditional proofs of mathematics. A formal proof is sufficiently detailed that its correctness can be verified mechanically. In contrast, a traditional mathematical proof can be thought of as a blueprint that provides just enough information to allow a well-trained reader to construct a formal proof. In fact, formal proofs are more prevalent in computer science than in mathematics. The most obvious reason is that only formal methods can be mechanized soundly. A more subtle reason, however, is the different nature of the proof task. Mathematical conjectures often contain no hint of w

Publisher

Cambridge University Press

Published

1998

Language

EN