Dear all, I am still experimenting with programming language semantics using both HOL Light and HOL4. My question is not specific to any of these two implementations, but I could not find any better place to ask, sorry.
I am following the HOL Light tutorial, where the weakest preconditions `wp`are derived from inductively defined big-step operational semantics. I want to prove that `wp (While e c) q` is the least fixed point: wp (While e c) q = lfp (λw. e AND wp c w OR NOT e AND q) but I can only prove that the right hand side implies the left hand side. Can you point me to a proof, ideally in HOL, of the above equivalence? The code from HOL Light tutorial is similar to the what Harrison describes in "Formalizing Dijkstra." He says "We could in fact prove that `Do gcs` is the least fixpoint," but do not give a proof (page 12). Dijkstra and Scholten give a proof in their "Predicate calculus and program semantics," but they heavily depend on their own notation and I found their reasoning difficult to mechanize in HOL. On the other extreme, HOL mechanizations of the refinement calculus simply define the weakest precondition for While as the least fixpoint. -- Piotr Trojanek ------------------------------------------------------------------------------ New Year. New Location. New Benefits. New Data Center in Ashburn, VA. GigeNET is offering a free month of service with a new server in Ashburn. Choose from 2 high performing configs, both with 100TB of bandwidth. Higher redundancy.Lower latency.Increased capacity.Completely compliant. vanity: www.gigenet.com _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
