A sound and relatively* complete Hoare-logic for a language with higher type procedures

DOI10.1007/BF00264295zbMath0501.68008MaRDI QIDQ1172384

Bernhard Josko, Werner Damm

Publication date: 1983

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

zbMATH Keywords

oracle setlanguage with procedures of finite modes and without global variablesrelatively complete Hoare-style proof-system

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items

An observationally complete program logic for imperative higher-order functions ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Fifty years of Hoare's logic ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Correctness of programs with Pascal-like procedures without global variables