SRC Research Report 16
SRC Research Report 16This paper gives a self-contained account of a general calculus of program semantics, from first principles through the semantics of recursion. The calculus is like Dijkstra's guarded commands, but without the Law of the Excluded Miracle; like extended dynamic logic, but with a different approximation relation; like a relational calculus studied by deBakker, but with partial relations as well as total relations; like predicative programming, but with a more standard notion of total correctness. The treatment of recursion uses the fixpoint method from denotational semantics.
Back to the SRC Research Reports main page.