Publisher's Synopsis
This text synthesizes research in top-down program design and verification of program correctness. It shows how these techniques may be used in day-to-day programming with the PASCAL language. Many examples of programs and proof development, as well as an explanation of control and data structures, are provided. As a PASCAL programming text, it not only provides a self-contained introduction to the language, but also offers algorithms which operate on sophisticated data structures, and provides the full axiomatic definition of PASCAL in terms of proof rules.;Although an introductory course in programmming is required, no particular mathematical background is necessary beyond the basic idea of a mathematical proof. A sample of algorithms, including some examples from business data processing, is presented. This collection is supplemented by an extensive set of exercises.
