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. |
From inside the book
Results 1-3 of 31
Page 43
... tion will cause an effective decrease of t . Bearing in mind that t is a function of the current state , we can consider wp ( SL ;, t≤ 10 ) ( 8 ) This is a predicate involving , besides the coordinate variables of the state space ...
... tion will cause an effective decrease of t . Bearing in mind that t is a function of the current state , we can consider wp ( SL ;, t≤ 10 ) ( 8 ) This is a predicate involving , besides the coordinate variables of the state space ...
Page 51
... tion of the form x = x0 and y = y0 and ... should give rise to a pre - condi- tion implying x = x0 and y = y0 and . . . ” . We shall guarantee this by treating such quantities as " temporary constants " ; they 51 THE FORMAL TREATMENT OF ...
... tion of the form x = x0 and y = y0 and ... should give rise to a pre - condi- tion implying x = x0 and y = y0 and . . . ” . We shall guarantee this by treating such quantities as " temporary constants " ; they 51 THE FORMAL TREATMENT OF ...
Page 111
... tion leaves relations P1 and P2 invariantly true . ) and one input command that can inspect the colour of a pebble , viz . " buck ( i ) " for 1≤i≤N : when the computer program prescribes the evalua- tion of this function of type ...
... tion leaves relations P1 and P2 invariantly true . ) and one input command that can inspect the colour of a pebble , viz . " buck ( i ) " for 1≤i≤N : when the computer program prescribes the evalua- tion of this function of type ...
Contents
THE ROLE OF PROGRAMMING LANGUAGES | 7 |
PROGRAMMING LANGUAGE | 24 |
5 | 37 |
Copyright | |
12 other sections not shown
Other editions - View all
Common terms and phrases
active scope ALGOL 60 algorithm allsix alternative construct array variable assignment statement ax.dom ax.hib ax.lob begin glocon boolean bucket C.A.R. Hoare Cartesian product chapter ckey clockwise boundary colour computation context convex hull current hull decrease defined definition denote divisor domain Dutch national flag element empty End of note End of remark established Euclid's algorithm execution finite formal function GCD(x given greatest common divisor guaranteed implies initializing statement inner block inspected integer introduce invariant relation kfac Linear Search machine maximal strong component mechanism nondeterminacy oldfile operation pebble possible post-condition predicate transformer privar problem programming language q.high repetitive construct semantics separation of concerns sequence set(i shortest solution statement list subset termination theorem tion true ultraviolet branches vertex vertices violet branch vir int array virvar weakest pre-condition wlp(S wp(DO wp(IF wp(S wp(SL x.norm xnext y.key
References to this book
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 David S. Frankel No preview available - 2003 |