Email Gateway (Aug 19 2022 at 17:19): Email Gateway (Aug 19 2022 at 17:19):From: Piotr Trojanek <piotr.trojanek@gmail.com>
Hi David,
I am aware that I should not start from the first equation when
deriving the second one. That is why I was starting from big-step
semantics (from which also the first equation is derived).
-- Piotr
Email Gateway (Aug 19 2022 at 17:19):From: David Cock <david.cock@inf.ethz.ch>
Piotr,
OK, then from the first equation, you have that the weakest
precondition of the loop is a fixed point of the body (combined with the
guard). Depending on how you've defined 'weakest precondition',
shouldn't you be able to appeal to the fact that it is the weakest to
show that you must have the least fixed point? You just need to
appeal to the properties of the complete lattice of predicates.
David
Email Gateway (Aug 19 2022 at 17:19):From: Piotr Trojanek <piotr.trojanek@gmail.com>
David,
It was easy to show that the argument of lfp is a fixed point, but I
cannot show that it is the least one.
My 'weakest precondition' is defined in a standard way, i.e. like the
"wpt" in theory file for Concrete Semantics section 12.5.
Any extra hints? Maybe some textbook or a theory file?
Regards,
Piotr
Email Gateway (Aug 19 2022 at 17:19):From: David Cock <david.cock@inf.ethz.ch>
Piotr,
Give me a little bit, and I'll forward you something.
David
Email Gateway (Aug 19 2022 at 17:19):From: David Cock <david.cock@inf.ethz.ch>
OK, your immediate problem is that wp in the Concrete Semantics book is the weakest liberal precondition i.e. gfp rather than lfp. The proof structure will be identical, just a mirror image.
David.
Email Gateway (Aug 22 2022 at 09:07):From: Piotr Trojanek <piotr.trojanek@gmail.com>
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?
Email Gateway (Aug 22 2022 at 09:07):From: Peter Lammich <lammich@in.tum.de>
Hi Piotr.
Have you looked at this AFP-entry:
http://afp.sourceforge.net/entries/MonoBoolTranAlgebra.shtml
in particular the while-statement in Statement.thy might be interesting
for you.
Email Gateway (Aug 22 2022 at 09:07):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
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.
Email Gateway (Aug 22 2022 at 09:07):From: Piotr Trojanek <piotr.trojanek@gmail.com>
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...
Email Gateway (Aug 22 2022 at 09:07):From: David Cock <david.cock@inf.ethz.ch>
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
Last updated: Nov 21 2024 at 12:39 UTC