A Discipline of ProgrammingExecutional abstraction; The role of programming languages; States and their characterization; The characterization of semantics; The semantic characterization of a programming language; Two theorems; On the design of properly terminating; Euclid's algorithm revisited; The formal treatment of some small examples; The linear search theorem; The problem of the next permutation. 
What people are saying  Write a review
User ratings
5 stars 
 
4 stars 
 
3 stars 
 
2 stars 
 
1 star 

Review: A Discipline of Programming
User Review  Tao  Goodreadsthis is one of those books that i intended to read for years, and gave up each time after read through a dozen page or so. this time, i pushed through pattern matching chapter now.beautifully written ... Read full review
Review: A Discipline of Programming
User Review  Mason Stewart  GoodreadsDijkstra whipped my ass. Awesome book, very difficult. Putting this on my "ReRead in Five Years" shelf :D Read full review
Contents
O EXECUTIONAL ABSTRACTION l  1 
THE ROLE OF PROGRAMMING LANGUAGES  7 
ON NONDETERMINACY BEING BOUNDED  9 
Copyright  
18 other sections not shown
Common terms and phrases
abort abs(x ALGOL 60 allsix alternative construct argument array variable assignment statement ax.dom ax.hib ax.lob begin glocon boolean C.A.R. Hoare Cartesian product chapter ckey clockwise boundary computation concurrent assignment convex hull decrease defined definition denote domain Dutch national flag edges element empty End of note established Euclid's algorithm execution expression face final state satisfying finite formal function GCD(x given glovar greatest common divisor guaranteed guarded command set guards is true implies initial state satisfying inner block inspected integer introduce invariant relation kfac Linear Search machine maximal strong component mechanism operation pebble possible postcondition predicate transformer privar problem programming language q.high repetitive construct separation of concerns sequence solution space statement list subset syntactic category termination theorem tion ultraviolet branches vertex vertices violet branch vir int array virvar weakest precondition wlp(S wp(DO wp(IF wp(S wp(SL y.key
References to this book
Logic in Computer Science: Modelling and Reasoning about Systems Michael Huth,Mark Ryan Limited preview  2004 
Model Driven Architecture: Applying MDA to Enterprise Computing David Frankel No preview available  2003 