Re: Reconciling Seqents and Hoare Triples

Dear Tim,

The book *Concrete Semantics*, by Gerwin Klein and Tobias Nipkow, gives a
nice introduction to reasoning about programs in a proof assistant. It has
a chapter on Hoare logic. It is available free online:

  http://www.concrete-semantics.org/concrete-semantics.pdf

Best wishes,

Jeremy



On Sat, Jun 24, 2017 at 1:07 AM, Tim Daly <[email protected]> wrote:

> 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
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer