Boogie's w.p. generation

Apr 14, 2014 at 9:07 PM
Hello, I have a question about Boogie's w.p. generation. According to the documentation, Boogie allows procedure declarations without an implementation. So something like
proc p(..)
requires: Pre()
ensures: Post()
My question is given an occurrence of p in some code,
x := 1;
p(..);
y : = 2
how does Boogie establish the w.p. of this code wrt to some postcondition Q?
Developer
Apr 30, 2014 at 10:28 PM
Hi snedunuri

On 14/04/2014 22:07, snedunuri wrote:

From: snedunuri

Hello, I have a question about Boogie's w.p. generation. According to the documentation, Boogie allows procedure declarations without an implementation. So something like
proc p(..)
requires: Pre()
ensures: Post()
My question is given an occurrence of p in some code,
x := 1;
p(..);
y : = 2

You can imagine the above first being transformed into:

x := 1;
assert Pre;
havoc(anything which p may modify);
assume Post;
y := 2;

The WP for this sequence is then constructed.

I'm attaching a deck of lecture slides which I have used to explain this - I hope they are useful.

Cheers

Ally


how does Boogie establish the w.p. of this code wrt to some postcondition Q?

May 13, 2014 at 2:42 AM
hi Ally, thanks. You wrote "I'm attaching a deck of lecture slides which I have used to explain this - I hope they are useful." But I don't see them attached

thanks