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

sav07_homework_4_solution.txt · Last modified: 2007/06/16 22:12 by vkuncak

© EPFL 2018 - Legal notice 