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,