Reconciling Seqents and Hoare Triples

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Reconciling Seqents and Hoare Triples

Tim Daly
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Reconciling Seqents and Hoare Triples

Jeremy Avigad
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:


Best wishes,

Jeremy



On Sat, Jun 24, 2017 at 1:07 AM, Tim Daly <[hidden email]> 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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Reconciling Seqents and Hoare Triples

Tim Daly
Thanks. Looks like I'll have to deep dive into HOL.

Tim


On Sat, Jun 24, 2017 at 5:03 AM, Jeremy Avigad <[hidden email]> wrote:
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:


Best wishes,

Jeremy



On Sat, Jun 24, 2017 at 1:07 AM, Tim Daly <[hidden email]> 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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer