Floyd-Hoare Logic Defines Semantics
The first-order patrial correctness assertions provable in Floyd-Hoare logic about an uninterpreted while-program scheme determine the scheme up to equivalence. This settles an open problem of Meyer and Halpern. The simple proof of this fact carries over to other partial correctness axiomatizations...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149117 |