Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A better weakest precondition rule for a condi...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:14):

From: scott constable <sdconsta@syr.edu>
I'm using the weakest precondition generator that comes with AutoCorres,
and I'm finding it lacking. In particular, the weakest precondition rule
"condition_wp"

{Q} A {P} ==> {R} B {P} ==> {\s. if C s then Q s else R s} condition C A B
{P}

is not useful when, for instance, post-condition P of B is dependent not
only on pre-condition R, but also on !C. So I tried writing an alternative
rule,

{\s. C s /\ Q s} A {P} ==> {\s. !C s /\ R s} B {P}
==> {\s. if C s then C s /\ Q s else !C s /\ R s} condition C A B {P}

I can prove this rule just fine, but now the weakest precondition generator
yields many more subgoals (with the original rule, it generates only 1).

Any suggestions? Is the existing condition_wp rule sufficient, and I'm just
not using it correctly?

Thanks in advance,

Scott Constable

Last updated: Apr 26 2024 at 12:28 UTC