Carroll Morgan Programming from Specifications Second Edition © Carroll Morgan 1990, 1994 and 1998. Permission is granted to copy this material for private study; for other uses please contact the author.

		About this web edition
		Preface
		Differences from the first edition
		Acknowledgements
		Contents
	1.	Programs and refinement
	2.	The predicate calculus
	3.	Assignments and sequential composition
	4.	Alternation
	5.	Iteration
	6.	Types and declarations
	7.	Case study: Square root
	8.	Initial variables
	9.	Constructed types
	10.	Case study: Insertion Sort
	11.	Procedures and parameters
	12.	Case study: Heap sort
	13.	Recursive procedures
	14.	Case study: The Gray code
	15.	Recursive types
	16.	Modules and encapsulation
	17.	State transformation and data refinement
	18.	Case study: Majority voting
	19.	Origins and conclusions
	20.	Case study: A paragraph problem
	21.	Case study: The largest rectangle under a histogram
	22.	Case study: A mail system
	23.	Semantics
	A.	Some laws for predicate calculation
	B.	Answers to some exercises
	C.	Summary of laws
		References
		Index
		Answers to all exercises
		The whole text (500K)
		Back to the top.

Look here, here or here for other formal methods material.