Difference between revisions of "Paper/Laws of programming"
Jump to navigation
Jump to search
(Created page with "{{cite journal |last= Hoare |first= C. A. R. |last2= Hayes |first2= I. J. |last3= He |first3= Jifeng |last4= Morgan |first4=C. C. |last5=Roscoe |first5=A. W. |last6=San...") |
|||
Line 23: | Line 23: | ||
|url=http://www.cs.ox.ac.uk/people/bill.roscoe/publications/20.pdf | |url=http://www.cs.ox.ac.uk/people/bill.roscoe/publications/20.pdf | ||
|publisher=ACM | |publisher=ACM | ||
|vol=30 | |||
|No=8 | |||
}} | }} | ||
Line 34: | Line 36: | ||
=Abstract= | =Abstract= | ||
A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications. | A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications. | ||
One should also watch [[Dana Scott]]'s lectures on <math>\lambda</math> calculus<ref>[[Dana Scott on Lambda Calculus]]</ref>. | |||
=References= | =References= | ||
<references/> | <references/> | ||
</noinclude> | </noinclude> |
Revision as of 04:28, 20 January 2022
Hoare, C. A. R.; Hayes, I. J.; He, Jifeng; Morgan, C. C.; Roscoe, A. W.; Sanders, J. W.; Sorensen, I. H.; Spivey, J. M.; Sufrin, B. A. (Aug 1987). "Laws of Programming" (PDF). ACM. Unknown parameter |vol=
ignored (|volume=
suggested) (help); Unknown parameter |No=
ignored (help)
Abstract
A complete set of algebraic laws is given for Dijkstra's nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott's domain theory as fixed points of continuous functionals. A calculus analogous to weakest preconditions is suggested as an aid to deriving programs from their specifications.
One should also watch Dana Scott's lectures on calculus[1].