a Practical Theory of Programming - University of Toronto

1 APracticalTheoryofProgramming2021-3-15 editionEric Hehner 5aPracticalTheoryofProgramming2021-3-15 editionEric HehnerDepartment of Computer ScienceUniversity of TorontoToronto ON M5S 2E4 CanadaThe first edition of this book was published bySpringer-Verlag Publishers, New York, 1993 ISBN 0-387-94106-1 current edition is available free ~hehner/aPToPAn on-line course based on this book is ~hehner/FMSDThe author's website ~hehnerYou may copy all or part of this book freely as long as you include this cover picture is an inukshuk, which is a human-like figure made of piled stones.

2 Inukshuks are found throughout arctic Canada. They are built by theInuit people, who use them to mean You are on the right path.. and Proof and Proof and Theory132 Basic Data Theory (optional) Structures223 Function Function and Fine Points (optional) Inclusion and Equality (optional) Functions (optional) Composition (optional) as and Reals (optional)334 Program (optional) Exponentiation45 and Completeness (optional) Space645 Programming with and Space (optional) (optional) Programming (optional) Number (optional) Programming (optional)

3 Refinement896 Recursive Data and Data Program Program Definition99 Contents 27 Theory Design and Data-Stack Program-Stack Program-Stack a and Completeness (optional) of Independent to Parallel and Communication (optional) Data Design and Data Design and and End of Contents 00 IntroductionWhat good is a Theory of Programming ?

4 Who wants one? Thousands of programmers program every day without any Theory . Why should they bother to learn one? The answer is the same as for any other Theory . For example, why should anyone learn a Theory of motion? You can move around perfectly well without one. You can throw a ball without one. Yet we think it important enough to teach a Theory of motion in high answer is that a mathematical Theory gives a much greater degree of precision by providing a method of calculation. It is unlikely that we could send a rocket to Jupiter without a mathematical Theory of motion.

5 And even baseball pitchers are finding that their pitch can be improved by using some Theory . Similarly a lot of mundane Programming can be done without the aid of a Theory , but the more difficult Programming is very unlikely to be done correctly without a good Theory . The software industry has an overwhelming experience of buggy programs to support that statement. And even mundane Programming can be improved by the use of a answer is that a Theory provides a kind of understanding.

6 Our ability to control and predict motion changes from an art to a science when we learn a mathematical Theory . Similarly Programming changes from an art to a science when we learn to understand programs in the same way we understand mathematical theorems. With a scientific outlook, we change our view of the world. We attribute less to spirits or chance, and increase our understanding of what is possible and what is not. It is a valuable part of education for engineering maintains its high reputation in our society by insisting that, to be a professional engineer, one must know and apply the relevant theories.

7 A civil engineer must know and apply the theories of geometry and material stress. An electrical engineer must know and apply electromagnetic Theory . Software engineers, to be worthy of the name, must know and apply a Theory of subject of this book sometimes goes by the name Programming methodology , science of Programming , logic of Programming , Theory of Programming , formal methods of program development , or verification . It concerns those aspects of Programming that are amenable to mathematical proof.

8 A good Theory helps us to write precise specifications, and to design programs whose executions provably satisfy the specifications. We will be considering the state of a computation, the time of a computation, the memory space required by a computation, and the interactions with a computation. There are other important aspects of software design and production that are not touched by this book: the management of people, the user interface, documentation, and the first usable Theory of Programming , often called Hoare's Logic , a specification is a pair of predicates: a precondition and postcondition (these and all technical terms will be defined in due course).

9 A closely related Theory uses Dijkstra's weakest precondition predicate transformer, which is a function from programs and postconditions to preconditions, further advanced in Back's Refinement Calculus. Jones's Vienna Development Method has been used to advantage in some industries; in it, a specification is a pair of predicates (as in Hoare's Logic), but the second predicate is a relation. There are theories that specialize in real-time Programming , some in probabilistic Programming , some in interactive Programming .

10 0 Introduction1 The Theory in this book is simpler than any of those just mentioned. In it, a specification is just a binary expression. Refinement is just ordinary implication. This Theory is also more comprehensive than those just mentioned, applying to both terminating and nonterminating computation, to both sequential and parallel computation, to both stand-alone and interactive computation. All at the same time, we can have variables whose initial and final values are all that is of interest, variables whose values are continuously of interest, variables whose values are known only probabilistically, and variables that account for time and space.