, Special issue on continuations. LISP and Symbolic Computation, vol.6, issue.1, pp.1993-1994
, A logic of object-oriented programs, TAPSOFT '97: Theory and Practice of Software Development, n umber 1214 in Lecture Notes in Computer Science, pp.682-696, 1997.
, Proof rules for gotos, Acta Informatica, vol.11, pp.139-148, 1979.
DOI : 10.1007/bf00264021
, Correct and robust programs, IEEE Transactions on Software Engineering, SE, vol.10, issue.2, pp.163-174, 1984.
, A Discipline of Programming, 1976.
, Programming Language Theory and its Implementation, N.J, 1988.
, Connection between Dijkstra's predicate transformers and denotational continuation semantics, 1978.
, Ecstatic: An object-oriented programming language with an axiomatic semantics, 4th Intl. Workshop on Foundations of Object Oriented L anguages 1997, 1997.
, Proof theory for exception handling in a tasking environment, Acta Informatica, vol.28, pp.7-41, 1990.
, Semantics with Applications: A Formal Introduction, 1992.
, Denotational Semantics: A Methodology for Language Development, 1986.
, The Formal Semantics of Programming Languages -An I n t r oduction. F oundations of Computing Series, 1993.
, Algorithm Gen(HHCCRV) = ( Q 0 F A U ), where: Gen(HH skip R V ) = ( RR skip V )
, Gen
, Q 0 F 1 F 2 A 1 A 2 U ) if Gen(HHC 2 R V ) = ( QQ F 2 A 2 W ) and Gen
, ) = (B ^ P 1 _ : B ^ P 2 F 1 F 2 if B then A 1 else A 2 U ) if Gen(HHC 1 R V ) = ( P 1 F 1 A 1 W ) and Gen, Gen
, Q ^ B) _ (R ^ : B)g fXg while B do A U ) if Gen(HHCCXXV f Xg) = ( QQ F AA U), for some X 2 V n V Gen
, HHtrap in C 1 with C 2 R V ) = ( Q 0 F 1 F 2 trap in A 1 with A 2 U ) if Gen(HHC 2 R V ) = ( QQ F 2 A 2 W ) and Gen(H Q==, Gen
, Gen
, HHbegin 1 : C 1 : : : n : C n end R V ) = (X 1 F beginfX 1 g 1 : A 1 : : : fX n g n : A n end U )
, for some X, vol.1