Weakly expressive models for Hoare logic

DOI10.1016/0304-3975(91)90232-QMaRDI QIDQ805248zbMATH OpenFDO

Authors R. Hoofman

Publication date 1991

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90232-Q

zbMATH Keywords

complete modelsexpressive modelsHoare logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The author generalizes the notion of complete models for Hoare logic to the weakly expressive models. After some preliminaries about Hoare logic, the author introduces the weakly expressive models and proves some important features of them. The main results are that the complete models are weakly expressive and that a model is expressive if the domain of every program is definable.

Recommendations

• scientific article; zbMATH DE number 3855074
• Weakly algebraizable logics
• Model theoretical aspects of weakly aggregative modal logic
• A Modal Extension of Weak Generalisation Predicate Logic
• Models of -calculus and the weak MSO logic
• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 4135914
• scientific article; zbMATH DE number 2154396
• Bisimulation for weakly expressive coalgebraic modal logics
• scientific article; zbMATH DE number 4147555

Cites work

• A New Incompleteness Result for Hoare's System
• An axiomatic basis for computer programming
• Definability by programs in first-order structures
• Effective Axiomatizations of Hoare Logics
• Expressiveness and the completeness of Hoare's logic
• Hoare's logic for programming languages with two data types
• scientific article; zbMATH DE number 3707731 (Why is no real title available?)
• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
• Some questions about expressiveness and relative completeness in Hoare's logic
• Soundness and Completeness of an Axiom System for Program Verification

This page was built for publication: Weakly expressive models for Hoare logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q805248)