All, Forgive my lack of deep understanding but I need guidance.
Consider trying to prove a program. The Sequent-style calculus of proofs are of the form: A -- B whereas the Hoare triple calculus is of the form A { Q } B Hoare makes the observation that "axioms may provide a simple solution to the problem of leaving certain aspects of the language undefined". Dijkstra [0] observes "This remark is deeper than the primarily suggested applications such as leaving wordlength or precise rounding rules unspecified. Hoare's rules for the repetitive construct rely on the fact that the repeatable statement leaves a relevant relation invariant. As a result, the same macroscopic proof is applicable to two different programs that only differ in the form of the repeatable statements S1 and S2, provided that both S1 and S2 leave the relation invariant (and ensure progress in the same direction). Clearly the statements in Q can be proven using sequent calculus. But Dijkstra hints at a "Giant Step" kind of reasoning and proof that enables one to skip the proof of Q, which would greatly simplify program proofs, especially mathematical proofs in Axiom. Consider that, in Axiom, I'm working at a proof from both ends. On one hand I have the code and on the other I have the mathematics. Sequent logic seems to insist on stepping through every line of the program. Hoare logic seems to imply that it is possible to ignore portions of the program logic provided the Q invariant holds. Clearly I need to do further study. Can you recommend any papers that might give me more clarity on this subject? Many thanks, Tim [0] Dijkstra, Edsger W. "Correctness Concerns and, among Other Things, Why They Are Resented" in Programming Methodology Springer-Verlag David Gries (ed) (1978) ISBN 0-387-90329-1 pp80--88
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer