Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems

DOI10.1145/322108.322121zbMath0388.68008OpenAlexW2140295918WikidataQ114614039 ScholiaQ114614039MaRDI QIDQ4170195

Publication date: 1979

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/322108.322121

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Algorithms in computer science (68W99) Computability and recursion theory on ordinals, admissible sets, etc. (03D60)

Related Items (32)

Stratified least fixpoint logic ⋮ Ernst-Rüdiger Olderog: A Life for Meaning ⋮ Verification conditions are code ⋮ Specifications in an arbitrary institution ⋮ Arithmetical completeness versus relative completeness ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Complexity of proving program correctness ⋮ Horn Clause Solvers for Program Verification ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ The Birth of Model Checking ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Verification of object-oriented programs: a transformational approach ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Hierarchical development of programming languages ⋮ On termination problems for finitely interpreted ALGOL-like programs ⋮ Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ A Hoare-like verification system for a language with an exception handling mechanism ⋮ Semantics and reasoning with free procedures ⋮ SMT-based model checking for recursive programs ⋮ Reasoning about procedures as parameters in the language L4 ⋮ Fifty years of Hoare's logic ⋮ On the Completeness of Dynamic Logic ⋮ Program invariants as fixedpoints ⋮ Semantics of algorithmic languages ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Completeness of algorithmic logic ⋮ Completeness of Hoare-calculi revisited ⋮ On the notion of expressiveness and the rule of adaptation ⋮ Proving program inclusion using Hoare's logic ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ Average case optimality for linear problems ⋮ Expressiveness and the completeness of Hoare's logic

This page was built for publication: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems