An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic (Q910396)
From MaRDI portal
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
