Hoare's Logic Is Not Complete When It Could Be
It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of part...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149036 |