LARA

Task 1

The property

r \circ (s \cap t) \subseteq (r \circ s) \cap (r \circ t)

holds. Namely, suppose (x,z) \in r \circ (s \cap t). Then there is a y such that (x,y) \in r and (y,z) \in s \cap t . Therefore, (y,z) \in s and (y,z) \in t. From (x,y) \in r and (y,z) \in s we have (x,z) \in r \circ s. Similarly, from (x,y) \in r and (y,z) \in t we have (x,z) \in r \circ t. Therefore, (x,z) \in (r \circ t) \cap (r \circ s).

Task 2

The property

(r \circ s) \cap (r \circ t) \subseteq r \circ (s \cap t)

does not hold. As an example, take A={1,2}, B={p,q} and let

\begin{array}{l} r = A \times A \\ s = \{(1,p),(2,q)\} \\ t = \{(1,q),(2,p)\} \end{array}

Task 3

(Sketch). By definitions of composition and inverse, both sides reduce to

\{(z,x) \mid \exists y. (x,y) \in r \land (y,z) \in s \}

Task 4

One way to prove it is to note that in the condition {P}r{Q}

(\forall s_1,s_2.\ (s_1 \in P \land (s_1,s_2) \in r)\ \rightarrow\ s_2 \in Q)

we can move quantification over s_2 inside and use properties of conjunction and implication to state it as:

\forall s_1.\ (s_1 \in P \rightarrow\ (\forall s_2.\ (s_1,s_2) \in r \rightarrow\ s_2 \in Q))

which is then equivalent to

P \subseteq \{ s_1 \mid \forall s_2. (s_1,s_2) \in r \rightarrow s_2 \in Q)

Therefore, the preconditions are precisely all subsets of the set on the right hand side, and so this set is the largest of them.

Alternatively, we can prove this property by showing by definition that 1) wp is a precondition and 2) that if we take any other precondition, it will be a subset of wp.

Task 5

The property

wp(r,Q_1 \cup Q_2) = wp(r,Q_1) \cup wp(r,Q_2)

does not hold in general. As a counterexample, take three distinct states s_1, s_2, and s_3, and let

\begin{array}{l} r = \{ (s_1,s_2), (s_1,s_3) \} \\ Q_1 = \{ s_2 \} \\ Q_2 = \{ s_3 \} \end{array}

Note: the property does hold for deterministic relations.

Task 6

The property

wp(r,Q_1 \cap Q_2) = wp(r,Q_1) \cap wp(r,Q_2)

is true and follows from the characterization of wp in Task 4 and the distribution of the right-hand side of implication and universal quantification with respect to conjunction.