- English only

# Lab for Automated Reasoning and Analysis LARA

### Forward and backward propagation

Let denote the result of propagating backward the error conditions, that is, the negation of postcondition. We define by

for all . Here for any set of states we write for the complement of , that is, the set .

If is the postcondition operator, that is,

**1.** Then show that

where denotes the inverse of relation . In other words, computing weakest preconditions corresponds to propagating possible errors backwards.

### Galois Connection

In the lecture we talked about a special case of Galois connection, called Galois insertion. Galois connection is in general defined by two monotonic functions and between partial orders on and on , such that

for all and (intuitively, the condition means that is approximated by ).

**2.** Show that the condition is equivalent to the conjunction of these two conditions:

hold for all and .

**3.** Let and satisfy the condition of Galois connection. Show that the following three conditions are equivalent:

- for all
- is a surjective function
- is an injective function

**4.** State the condition for to hold for all . When is the set of sets of concrete states and is a domain of static analysis, is it more reasonable to expect that or to be satisfied, and why?