A Discipline of Programming
Executional 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.
Results 1-3 of 33
Now wp("a: = a + d", P) = ((a + d)2 < n and b2 > n) which, because P implies the
second term, leads to the first term as our first guard; the second guard is derived
similarly and our next form is a, b:=0,n + 1; do a + 1 ^ b — > d: = . . . ; if (a + d)2 ...
The easy step is that the right-hand side of (2) implies its left-hand side. For,
consider an arbitrary point X in state space, such that the right-hand side of (2)
holds, i.e. there exists a nonnegative value, s' say, such that in point X the relation
substituting (4) and (5), we find (xl + yl)*(x2 + y2) = (xl * x2)+(xl * y2)+(yl * x2)+(yl *
y2) = 0 which implies the right-hand side of (6). To show that the right-hand side
of (6) implies its left-hand side, we have to show that it implies zl * z2 = 0 and Z ...
What people are saying - Write a review
LibraryThing ReviewUser Review - mykl-s - LibraryThing
-helped make me a good programmer -It 's about simplicity and clarity and about designing first, then writing -not an easy read, but well worth it Read full review
LibraryThing ReviewUser Review - MarkvanderPol - LibraryThing
One of the grandfathers of computer science. Lucid exploration of fundamental programming constructs that are still the daily tools of legions of programmers worldwide. If only they had the concept grounding from this book (or those like it) myriads of bugs would never be written. Read full review
Q THE FORMAL TREATMENT OF SOME SMALL
9 other sections not shown
Logic in Computer Science: Modelling and Reasoning about Systems
Michael Huth,Mark Ryan
No preview available - 2004
Model Driven Architecture: Applying MDA to Enterprise Computing
No preview available - 2003