conrad@wucs1.wustl.edu (H. Conrad Cunningham) (10/19/90)
A few days ago I asked for suggestions and comments concerning a textbook for a course in "program specification, derivation, and correctness verification". My candidates included: Gries' _The Science of Programming_ (Springer-Verlag, 1981) Dijkstra & Feijen's _A Method of Programming_ (Addison-Wesley, 1988) Dromey's _Program Derivation: The Development of Programs from Specifications_ (Addison-Wesley, 1989) Gumb's _Programming Logics_ (Wiley, 1989) The following are exerpts from the responses I have received to date or that I have seen posted. Since I didn't say I was posting the responses back to the bulletin boards, I deleted the names of the respondents. Additional suggestions are, of course, still welcome. - Conrad Cunningham, CIS Dept., University of Mississippi, USA cunningham@cs.olemiss.edu ------------------------------------------------------------------------------- You might consider _The Craft of Programming_ by John Reynolds (Prentice-Hall, 1981). I took his (advanced undergraduate) course on programming proving at CMU. I very much enjoyed both the course and the text. ---------- A new book that I particularly like is Carroll Morgan's _Programming from Specifications_ (Prentice-Hall, 1990) Carroll is at the Programming Research Group (PRG) Oxford - the book is used for teaching 2nd year students there. You can find an early reference in the IBM Journal of Research and Development 31(5) 1987 (Morgan & Robinson). ---------- Maybe you should also consider the recent book by Carroll Morgan _Programming from Specifications_ ... ---------- I taught a similar course and used Gries' "Science of Programming". It's fallen behind the field, but it is still a good introduction. You might add to your list: Dijkstra (ed.) Formal Development of Programs and Proofs (Addison-Wesley, 1990) ISBN 0-201-17237-2. This isn't so much a text as a collection of short papers. It does give some good examples of the Dijkstra/Gries method and of other methods as well. ---------- I have used Hehner's Logic of Programming (Prentice Hall 1984) successfully for this purpose for many terms. ---------- Well I like the Gries book a lot, but it is purely a classroom exercise book, and it does not deal well with the specification of systems as opposed to verification. By this I mean that its approach does not scale to real problems. Dijkstra suffers from the same problem (while also being insufferably ivory tower). It is important to make students realise that this stuff is not just pointless symbol pushing---something that neither of these books address; they are aimed at people already interested in theories and logic, and do not justify themselves well. Less elegant, but more useful as a way of convincing people that this sort of thing is useful in practise is Cliff Jones' book on VDM (the second edition) in Prentice Hall International Systematic Software Development in VDM It addresses the specification and reification issues much better. Carroll Morgan's `Programming from Specifications' (I think) in the same series might also be good (it uses Z rather than VDM) but I have not read it. The one I would recommend is Jones; it has the further advantage, which backs up the points I made above, in a companion volume which gives a collection of practical case studies that can be looked at as well. (Though Ian Hayes has also published a good collection of case studies for Z, again in PHI). --------- Ric Hehner's book ``The Logic of Programming'', is a bit more solid than Gries's book, and may be more appropriate for that level of students. Carroll Morgan has a recent book on the subject too. Both are published by Prentice-Hall in the series edited by Hoare. ---------- I strongly recommend that you consider Backhouse "Program Construction and Verification" (Prentice Hall, isbn: 0-13-729153-1). It uses a simplified Pascal language (rather than Gries' guarded commands a la Dijkstra) This has costs (some programs are less clean) but also reduces the overhead on students limited conceptual powers! If your students are very good, you might also consider (after an elementary book like Gries or Backhouse) looking at Loekx and Sieber "Foundations of Program verification" (J. Wiley-Teubner) which covers denotational semantics and fix-point induction etc. ---------- I haven't had time to look at them closely, but consider: Carroll Morgan, _Programming from Specifications_ Prentice Hall International 1990 ISBN 0-13-726225-6 D. C. Ince, _An Introduction to Discrete Mathematics and Formal System Specification_ Clarendon Press 1988 ISBN 0-19-859667-7 ---------- You might take a look at Carroll Morgan's _Programming from Specifications_. ----------