[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Reconciling Seqents and Hoare Triples

From: Jeremy Avigad
Subject: Re: [Axiom-developer] Reconciling Seqents and Hoare Triples
Date: Sat, 24 Jun 2017 10:03:30 +0100

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,


On Sat, Jun 24, 2017 at 1:07 AM, Tim Daly <address@hidden> wrote:

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:


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

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,

[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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]