An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic

DOI10.1305/NDJFL/1093635239MaRDI QIDQ910396zbMATH OpenOpenAlexFDO

Authors Ildikó Sain

Publication date 1989

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1093635239

zbMATH Keywords

Floyd-Hoare logicnondeterministic programsrelational tracessecond-order logicsemanticstime-models

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

A simpler and more direct proof of Csirmaz's model-theoretic characterization of Floyd-Hoare logic for nondeterministic programs is presented. As a spin-off, a straightforward proof of Leivant's characterization of this logic in terms of second-order logic is also given. Finally, a direct connection between Czirmaz's ``relational traces and ``time-models for nondeterministic programs is established.

Recommendations

• Strong Semantical Characterization for Nondeterministic Programs
• scientific article; zbMATH DE number 3921949
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• scientific article; zbMATH DE number 4200180
• Logical analysis of demonic nondeterministic programs

Cited in

(6)

• Inductive completeness of logics of programs
• On the Completeness of Dynamic Logic
• scientific article; zbMATH DE number 3921949 (Why is no real title available?)
• Strong Semantical Characterization for Nondeterministic Programs
• Total correctness in nonstandard logics of programs
• On the strength of temporal proofs

This page was built for publication: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic

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