Re: [isabelle] Weakest precondition of WHILE as a least fixed point
One problem that you're likely to run into here is that the first
equation that you quote is not definitional: It's an equality that holds
for the denotation that you're after, but also for (potentially
infinitely many) others, every fixed point of the loop body, in fact.
To go from the first equation to the second requires you to make a
choice - to state that you want to interpret a loop as the *least* fixed
point of its body. This is not implied, it's sometimes useful to take
the greatest fixed point, for example to derive a
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:
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.
On 10 Mar 2015, at 9:48 pm, Piotr Trojanek <piotr.trojanek at gmail.com> wrote:
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
I was trying to prove this derivation, but always ended in a loop. Any advice?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and