All, Forgive my lack of deep understanding but I need guidance. -- 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 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 |
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:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Thanks. Looks like I'll have to deep dive into HOL. On Sat, Jun 24, 2017 at 5:03 AM, Jeremy Avigad <[hidden email]> wrote:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |