An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic.
Ildikó Sain · Notre Dame Journal of Formal Logic · 1989
We give a relatively simple and direct proof for Csirmaz's characterization of Floyd-Hoare logic for nondeterministic programs [5].(This also yields a very simple proof for Leivant's characterization [13].)We also establish a direct connection between "relational traces" and "time-models" for nondeterministic programs.