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 <axiom...@gmail.com> 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 Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
