# Reconciling Seqents and Hoare Triples

3 messages
Open this post in threaded view
|

## Reconciling Seqents and Hoare Triples

 All,Forgive my lack of deep understanding but I need guidance.Consider trying to prove a program. The Sequent-style calculusof proofs are of the form:      A      --      Bwhereas the Hoare triple calculus is of the form    A { Q } BHoare makes the observation that "axioms may provide a simplesolution to the problem of leaving certain aspects of the languageundefined".Dijkstra [0] observes "This remark is deeper than the primarilysuggested applications such as leaving wordlength or preciserounding rules unspecified. Hoare's rules for the repetitive constructrely on the fact that the repeatable statement leaves a relevantrelation invariant. As a result, the same macroscopic proof isapplicable to two different programs that only differ in the form ofthe repeatable statements S1 and S2, provided that both S1 and S2leave 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 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,Why They Are Resented" in Programming Methodology Springer-VerlagDavid Gries (ed) (1978) ISBN 0-387-90329-1  pp80--88 _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer