|
From: | Jeremy Avigad |
Subject: | Re: [Axiom-developer] Reconciling Seqents and Hoare Triples |
Date: | Sat, 24 Jun 2017 10:03:30 +0100 |
Why They Are Resented" in Programming Methodology Springer-Verlagleave the relation invariant (and ensure progress in the same direction).the repeatable statements S1 and S2, provided that both S1 and S2applicable to two different programs that only differ in the form ofrelation invariant. As a result, the same macroscopic proof isrely on the fact that the repeatable statement leaves a relevantrounding rules unspecified. Hoare's rules for the repetitive constructsuggested applications such as leaving wordlength or preciseDijkstra [0] observes "This remark is deeper than the primarilyundefined".solution to the problem of leaving certain aspects of the languageHoare makes the observation that "axioms may provide a simpleA { Q } Bwhereas the Hoare triple calculus is of the formBAof proofs are of the form:All,Consider trying to prove a program. The Sequent-style calculus
Forgive my lack of deep understanding but I need guidance.
--Clearly the statements in Q can be proven using sequent calculus.But Dijkstra hints at a "Giant Step" kind of reasoning and proof thatenables one to skip the proof of Q, which would greatly simplify programproofs, especially mathematical proofs in Axiom.Consider that, in Axiom, I'm working at a proof from both ends. On onehand I have the code and on the other I have the mathematics.Sequent logic seems to insist on stepping through every line of theprogram. Hoare logic seems to imply that it is possible to ignore portionsof the program logic provided the Q invariant holds.Clearly I need to do further study. Can you recommend any papers thatmight give me more clarity on this subject?Many thanks,Tim[0] Dijkstra, Edsger W. "Correctness Concerns and, among Other Things,
David Gries (ed) (1978) ISBN 0-387-90329-1 pp80--88
[Prev in Thread] | Current Thread | [Next in Thread] |