An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic (Q910396): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
| links / mardi / name | links / mardi / name | ||
Revision as of 17:01, 30 January 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic |
scientific article |
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
