Thanks. Looks like I'll have to deep dive into HOL. Tim
On Sat, Jun 24, 2017 at 5:03 AM, Jeremy Avigad <avi...@cmu.edu> 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: > > 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
