• English only

Lab for Automated Reasoning and Analysis LARA

This is a sketch of the solution of SAV07 Homework 4

Part 1

Then we have

.

Then we have .

Note that we have .

Basically, and both act as a left zeros of for the relations of the form .

Part 2

It is easiest to use the definition of Galois connection given by . The condition then reduces to

Both sides are equivalent to , that is, to the Hoare triple .

Part 3

is not a partial order, it is merely a preorder.

Part 4

Let denote . We then have and the statement reduces to proving the equivalence between

and

We prove both directions.

: Let . Take any such that . Then , so . Therefore .

: Let . Let . Then , so also . Thus .

Part 5

Lemma: .

: Let . Then by construction of , so by definition of we have , i.e. .

: Let . Then . By monotonicity of wp, also , so .

: Let . Then , so by basic set theory .

assume(F) skip assert(F), assert(F); assume(F) assert(F), assume(F); assert(F) assume(F) - follow from rules for computing weakest preconditions.

Part 6

Suppose . Then by Part 5 we have

Suppose . Then

Suppose . Then

Suppose . Then

Part 7

By shunting rules in Part 6 we have . By monotonicity properties in Part 5, we then obtain by structural induction.