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 (20)

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

This page was built for publication: Program proving: KJumps and functions