[OT[ proving programs for novices

David Bakin davidbak@windows.microsoft.com
Tue, 15 Apr 2003 14:51:03 -0700

How would this book relate - in subject, difficulty, audience - to:

	The Science of Programming by Gries?
	Algebra of Programming by Bird, De Moor, Moor?

Thanks!  - Dave

-----Original Message-----
From: Doaitse Swierstra [mailto:doaitse@cs.uu.nl]
Sent: Tuesday, April 15, 2003 12:38 PM
To: Bill Wood
Cc: Doaitse Swierstra; haskell-cafe@haskell.org
Subject: Re: [OT[ proving programs for novices

One might be interested in the newly published book by Roland=20
Backhouse: "Program Construction : Calculating Implementations from=20


I quote from the publishers web site:

"The ever-increasing dependence of our lives and livelihoods on the=20
correct functioning of computer software means that logic and program=20
correctness are core elements of all good computer science degrees.=20
This book presents both these topics in one self-contained text.

The focus of the book is on "correct-by-construction" program design --=20
the discipline of calculating programs from their specifications.=20
Modern, calculational logic is introduced in combination with key=20
program construction principles, such as the assignment axiom, loop=20
invariants and bound functions. This material is intertwined with=20
motivational discussion, programming examples and challenging=20
problem-solving exercises, bringing the book alive for its intended=20
audience, undergraduates in computer science and mathematics, as well=20
as professional programmers wishing to further develop their=20
programming skills.

The book covers the elements of logic and program correctness that form=20
the foundations of further study --- the logical connectives and their=20
algebraic properties, induction, quantifiers and program construction=20
rules. Substantial examples of program construction are included. Many=20
exercises are provided, all with detailed solutions.   "

  Doaitse Swierstra

Haskell-Cafe mailing list