An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic (Q910396)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic |
scientific article; zbMATH DE number 4139720
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic |
scientific article; zbMATH DE number 4139720 |
Statements
An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic (English)
0 references
1989
0 references
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.
0 references
semantics
0 references
Floyd-Hoare logic
0 references
nondeterministic programs
0 references
second-order logic
0 references
relational traces
0 references
time-models
0 references
