Program proving: KJumps and functions

DOI10.1007/BF00288686zbMath0229.68003OpenAlexW2142018213MaRDI QIDQ2550288

C. A. R. Hoare, Maurice Clint

Publication date: 1971

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00288686

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

A compositional natural semantics and Hoare logic for low-level languages, Unnamed Item, Hierarchical program specification and verification - a many-sorted logical approach, Weakest preconditioned goto axiom, On algebra of program correctness and incorrectness, Semantical analysis of specification logic, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, Proof theory for exception handling in a tasking environment, A mechanical analysis of program verification strategies, Continuations in possible-world semantics, An axiomatic basis for proving total correctness of goto-programs, Axiomatic semantics for escape statements, Axiomatic approach to side effects and general jumps, Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare, The use of Hoare's method of program verification for the Quicksort algorithm, Fifty years of Hoare's logic, Current methods for proving program correctness, Automatic program verification. I: A logical basis and its implementation, On verification of programs with goto statements, A complete axiomatic semantics of spawning

Uses Software

• ALGOL 60

Cites Work

• Notes on avoiding ``go to statements
• Correspondence between ALGOL 60 and Church's Lambda-notation
• An axiomatic basis for computer programming