hi. this isnt a haskell question but i am hoping you will forgive it. i was wondering where i could find books/websites/tutorials on how to construct proofs and how to prove programs. preferably books that are aimed at novices with some programming experience but little math/logic experience. i have paul hudaks hsoe book which has some material on proving properties of programs. sincerely chris moline
At 7:19 PM -0700 3/17/03, Chris Moline wrote:
hi. this isnt a haskell question but i am hoping you will forgive it.
i was wondering where i could find books/websites/tutorials on how to construct proofs and how to prove programs. preferably books that are aimed at novices with some programming experience but little math/logic experience.
For imperative programming: D. Gries, The Science of Programming. Springer Verlag, New York, 1981. E.W. Dijkstra, A Discipline of Programming. Prentice-Hall, 1975. For functional programming: R. Bird, Introduction to Functional Programming using Haskell, 2nd edition. Prentice-Hall, 1998. -- ------------------------------------------------------------------ Hamilton Richards Department of Computer Sciences Senior Lecturer The University of Texas at Austin 512-471-9525 1 University Station C0500 Taylor Hall 5.138 Austin, Texas 78712-1188 ham@cs.utexas.edu hrichrds@swbell.net ------------------------------------------------------------------
. . .
For imperative programming:
D. Gries, The Science of Programming. Springer Verlag, New York, 1981.
E.W. Dijkstra, A Discipline of Programming. Prentice-Hall, 1975.
These are two excellant sources; I've learned from each and taught from each. However, they are both a bit stiff for the student with little background in logic or mathematics. Several texts did come out in the late 80's that taught the same approach from a more elementary starting point. Three such are E.W.Dijkstra and W.H.J. Feijen, A Method of Programming, Addison-Wesley, 1988, ISBN 0-201-17536-3 Geoff Dromey, Program Derivation/The Development of Programs from Specifications, Addison-Wesley, 1989, ISBN 0-201-41624-7 Edward Cohen, Programming in the 1990s, Springer-Verlag, 1990, ISBN 0-387-97382-6
For functional programming:
R. Bird, Introduction to Functional Programming using Haskell, 2nd edition. Prentice-Hall, 1998.
I'd like to hear abut more sources here as well. I've started in on Richard Bird and Oege de Moor, Algebra of Programming, Prentice Hall,1997, ISBN 0-13-507245-X but it is hardly elementary! Another very interesting text is John Cooke, Constructing Correct Software/the basics, Springer-Verlag, 1988, ISBN 3-540-76156-X which almost combines imperative and functional programming (and logical) by presenting a method of transforming (logical) specifications through functions into imperative programs. -- Bill Wood wtwjek@winternet.com
One might be interested in the newly published book by Roland Backhouse: "Program Construction : Calculating Implementations from Specifications" http://www.wiley.com/remtitle.cgi?0470848820 I quote from the publishers web site: "The ever-increasing dependence of our lives and livelihoods on the correct functioning of computer software means that logic and program correctness are core elements of all good computer science degrees. This book presents both these topics in one self-contained text. The focus of the book is on "correct-by-construction" program design -- the discipline of calculating programs from their specifications. Modern, calculational logic is introduced in combination with key program construction principles, such as the assignment axiom, loop invariants and bound functions. This material is intertwined with motivational discussion, programming examples and challenging problem-solving exercises, bringing the book alive for its intended audience, undergraduates in computer science and mathematics, as well as professional programmers wishing to further develop their programming skills. The book covers the elements of logic and program correctness that form the foundations of further study --- the logical connectives and their algebraic properties, induction, quantifiers and program construction rules. Substantial examples of program construction are included. Many exercises are provided, all with detailed solutions. " Doaitse Swierstra
participants (4)
-
Bill Wood -
Chris Moline -
Doaitse Swierstra -
Hamilton Richards