Publication:

An elementary and unified approach to program correctness

Back RJR (1978) On the Correctness of Refinement Steps in Program Development. PhD thesis, University of Helsinki. Also available as report A-1978-5

Back RJR (1980) Correctness preserving program refinements: proof theory and applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam

Backhouse R (2003) Program Construction: Calculating Implementations from Specifications. Wiley, New York

Backhouse R, Fokkinga M (2001) The associativity of equivalence and the towers of Hanoi problem. Inf Process Lett 77(2–4): 71–76

Backhouse R, Michaelis D (2006) Exercises in quantifier manipulation. In: Uustalu T (eds) MPC, volume 4014 of Lecture Notes in Computer Science. Springer, Berlin, pp 69–81

Bohórquez JA (2007) An inductive theorem on the correctness of general recursive programs. Logic Journal of the IGPL 15(5–6): 373–399

Bohórquez JA (2008) Intuitionistic logic according to Dijkstra’s calculus of equational deduction. Notre Dame J Form Log 49(4): 361–384

Dijkstra EW, Feijen WHJ (1988) Een Methode van Programmeren. Academic Service, Den Haag, 1984. Also available as A Method of Programming. Addison-Wesley, Reading

Dijkstra EW (1968) Go to statement considered harmful. Commun ACM 11(3): 147–148

Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8): 453–457

Dijkstra EW (1976) A discipline of programming. Prentice-Hall Inc., Englewood Cliffs. With a foreword by C.A.R. Hoare, Prentice-Hall Series in Automatic Computation

Dijkstra EW (1994) How computing science created a new mathematical style. EWD 1073 in The writings of Edsger W. Dijkstra, 2000. http://www.cs.utexas.edu/users/EWD

Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Springer, Berlin

Dromey RG (1982) How to solve it by computer. Prentice Hall, Englewood Cliffs

Floyd RW (1967) Assigning meanings to programs. In: Proceedings of the symposium on applied mathematics, American Mathematical Society XIX:19–32

Feijen WHJ, van Gasteren AJM (1996) Programming, proving, and calculation. In: Neville Dean C, Hinchey MG (eds) Teaching and learning formal methods. Academic Press, New York

Gries D (1981) The science of programming. Springer, Berlin

Gries D, Schneider FB (1993) A logical approach to discrete math. Texts and Monographs in Computer Science. Springer, Berlin

Hehner ECR (1976) DO considered OD: a contribution to the programming calculus. Technical Report CSRG-75, University of Toronto, Computer Systems Research Group, Toronto

Hehner ECR (1984) Predicative programming. I, II. Commun ACM 27(2):134–143, 144–151

Hehner ECR (1989) Termination is timing. In: MPC: International conference on mathematics of program construction. LNCS, Springer, Berlin

Hehner ECR (1990) A practical theory of programming. Sci Comput Program 14(2–3): 133–158

Hehner ECR (2004) From boolean algebra to unified algebra. MATHINT: The Mathematical Intelligencer 26

Hehner ECR (2004) A practical theory of programming, 2nd edn. Springer, New York

Hehner ECR (2005) Specified blocks. In: Meyer B, Woodcock J (eds) VSTTE, volume 4171 of Lecture Notes in Computer Science. Springer, Berlin, pp 384–391

Hehner ECR (2006) Retrospective and prospective for unifying theories of programming. In: Dunne S, Stoddart B (eds) UTP, volume 4010 of Lecture Notes in Computer Science. Springer, Berlin, pp 1–17

Hehner ECR (2007) Unified algebra. Int J Math Sci (WASET) 1(1):20–37 (electronic)

Hoare CAR, Jifeng H (1987) The weakest prespecification. Inf Process Lett 24(2): 127–132

Hoare CAR, Jifeng H (1998) Unifying theories of programming. Prentice Hall, London

Hoare CAR (1969) An axiomatic basis for computer programming. Commun Assoc Comput Mach 12(10): 576–583

Hoare CAR (1983) An axiomatic basis for computer programming (reprint). Commun ACM 26(1): 53–56

Hoare CAR (1984) Programs are predicates. Philos Trans Roy Soc Lond Ser A 312(1522): 475–489

Hoare CAR (1992) Programs are predicates. In: Proceedings of the international conference on fifth generation computer systems, pp 211–218, ICOT, Japan, 1992. Association for Computing Machinery

Kaldewaij A (1990) Programming: the derivation of algorithms. International Series in Computer Science. Prentice-Hall, Englewood Cliffs

Lifschitz V (2001) On calculational proofs. Ann Pure Appl Logic 113(1–3): 207–224

Manna Z (1974) Mathematical theory of computation. McGraw-Hill, New York

Manna Z (1980) Lectures on the logic of computer programming. Philadelphia, PA. With contributions by N. Dershowitz and R. Waldinger

Morgan C (1990) Programming from specifications. Prentice Hall, Englewood Cliffs

Morris JM (1990) Programs from specifications. In: Dijkstra EW (eds) Formal development of programs and proofs. Addison-Wesley, Reading

Martin AJ, Rem M (1984) A presentation of the fibonacci algorithm. IPL: Inf Process Lett 19

van de Snepscheut Jan LA (1993) What computing is all about. Texts and monographs in computer science. Springer, New-York

van Gasteren AJM (1990) On the shape of mathematical arguments, volume 445 of Lecture Notes in Computer Science. Springer, Berlin

van Gasteren AJM, Bijlsma A (1998) An extension of the program derivation format. In: Gries D, Roever WP (eds) PROCOMET, volume 125 of IFIP conference proceedings. Chapman & Hall, London, pp 167–185

Wirth N (1971) Program development by stepwise refinement. Commun ACM 14: 221–227