*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Weakest precondition of WHILE as a least fixed point*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Thu, 12 Mar 2015 12:24:44 +0100*In-reply-to*: <CAGExNxHG_kViEu393sL4Y+47yJ8=MEjHshE3hzP659XLr7Tc2g@mail.gmail.com>*References*: <CAGExNxGLrPZbeRjx-CBg20zD2n8VHoJ_3Aktmxtdc_rbGt97LQ@mail.gmail.com> <B8D16B29-F316-4FB9-97EB-9C1DC06DB303@nicta.com.au> <CAGExNxHG_kViEu393sL4Y+47yJ8=MEjHshE3hzP659XLr7Tc2g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.4.0

Piotr,

David On 11/03/15 23:15, Piotr Trojanek wrote:

Thank you both for your answers. I am familiar with chapter 11 of Concrete Semantics. In section 12.3 you have (page 205): wp (WHILE b DO c) Q = (\s. if bval b s then wp (c ;; WHILE b DO c) Q s else Q s) but I need: wp (WHILE b DO c) Q = lfp (\w. b AND wp c w OR NOT b AND q) (where AND, OR and NOT are lifted Boolean operators). I was trying to get it from the denotational equation with lfp but failed. Maybe I should try harder? The second formulation is equivalent to that from HOL Light tutorial (section 17.2, while_def). I am still studying the AFP entry suggested by Peter... On Wed, Mar 11, 2015 at 9:28 PM, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:Hi Piotr, is the fixpoint formulation in chapter 11 of http://concrete-semantics.org what you are after? Traditionally, Hoare Logic and weakest precondition calculi do not really derive a weakest precondition for While, but rely on user-provided invariants instead, but I might be misunderstanding what you mean by weakest precondition. Cheers, GerwinOn 10 Mar 2015, at 9:48 pm, Piotr Trojanek <piotr.trojanek at gmail.com> wrote: Dear experts, I am experimenting with mechanized semantics of a simple imperative programming language. I have already seen a dozen of mechanizations which start from big-step semantics and derive the weakest precondition of WHILE expressed as a recursive equation (which is then used to derive Hoare rules). Instead, I would like to derive the weakest precondition of WHILE expressed as a least fixed point (which is more useful in the refinement calculus). I was trying to prove this derivation, but always ended in a loop. Any advice? -- Piotr Trojanek________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

**Follow-Ups**:**Re: [isabelle] Weakest precondition of WHILE as a least fixed point***From:*Piotr Trojanek

**References**:**[isabelle] Weakest precondition of WHILE as a least fixed point***From:*Piotr Trojanek

**Re: [isabelle] Weakest precondition of WHILE as a least fixed point***From:*Gerwin Klein

**Re: [isabelle] Weakest precondition of WHILE as a least fixed point***From:*Piotr Trojanek

- Previous by Date: [isabelle] QUANTIFY 2015: Call for Papers
- Next by Date: Re: [isabelle] Storing Generic_Data in a local theory
- Previous by Thread: Re: [isabelle] Weakest precondition of WHILE as a least fixed point
- Next by Thread: Re: [isabelle] Weakest precondition of WHILE as a least fixed point
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list