A Complete Axiomatic System for Proving Deductions About Recursive Programs
Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of a H u {^,v,∃,∀} uH^-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148924 |