Re: [isabelle] Weakest precondition of WHILE as a least fixed point



Piotr,
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 weakest-*liberal*-precondition semantics.

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,
Gerwin

On 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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.