Introduction

This is the Lab3 report by Mazdak and Tobias in the Testing, Debugging and Verification course at CTH.

Rules

$\begin{split} {wp\left(x :=e, R\right)} &= R[x \mapsto e] && {\ ({\mathbf{§1}})}\\ {wp\left(S1; S2, R\right)} &= {wp\left(S1, {wp\left(S2, R\right)}\right)} && {\ ({\mathbf{§2}})}\\ {wp\left({\text{assert }}B, R\right)} &= B {\ \land \ }R && {\ ({\mathbf{§3}})}\\ {wp\left({{if\left(B\right) \ \{ S1 \}} \ {else \ \{ S2 \}}}, R\right)} &= B \to {wp\left(S1, R\right)} {\ \land \ }\neg B \to {wp\left(S2, R\right)} && {\ ({\mathbf{§4}})}\\ {wp\left({if\left(B\right) \ \{ S1 \}}, R\right)} &= B \to {wp\left(S1, R\right)} {\ \land \ }\neg B \to R && {\ ({\mathbf{§5}})}\\ \end{split}$

Variable names:

$\begin{split} Q &: \text{Precondition}\\ R &: \text{Postcondition}\\ I &: \text{Loop invariant}\\ B &: \text{Loop branch condition}\\ V &: \text{Loop variant}\\ S &: \text{Statement inside loop}\\ \end{split}$

Ex1

Given: $\begin{split} Q &: {\varnothing}= {{\mathbf{\top}}}\\ R &: 0 \leq y {\ \land \ }(0 \leq x \to y = x) {\ \land \ }(x < 0 \to y = -x) \end{split}$

Then: $\begin{split} & {wp\left({{if\left(x < 0\right) \ \{ y := -x \}} \ {else \ \{ y := x \}}}, R\right)} \\ {\ ({\mathbf{§4}})} \iff & \left(x < 0 \to {wp\left(y:= -x, R\right)}\right) {\ \land \ }\left(0 \leq x \to {wp\left(y:= x, R\right)}\right)\\ {\ ({\mathbf{§1}})} \iff & (x < 0 \to (0 \leq -x {\ \land \ }(0 \leq x \to -x = x) {\ \land \ }(x < 0 \to -x = -x )))\\ \land & (x \leq 0 \to (0 \leq x {\ \land \ }(0 \leq x \to x = x) {\ \land \ }(x < 0 \to x = -x)))\\ \iff & (x < 0 \to -x = -x) {\ \land \ }(0 \leq x \to x = x)\\ \iff & {{\mathbf{\top}}}\\ \end{split}$

Therefore: $\begin{split}Q \implies& {{\mathbf{\top}}}\end{split}$

In other words, the postcondition holds for all possible preconditions.

Ex2

Given: $\begin{split} R &: big > small \end{split}$

Then: $\begin{split} & {wp\left({{if\left(x > y\right) \ \{ big, small := x, y \}} \ {else \ \{ big, small := y, x \}}}, R\right)} \\ {\ ({\mathbf{§4}})} \iff & (x > y \to {wp\left(big, small := x, y, R\right)}) {\ \land \ }(x \leq y \to {wp\left(big, small := y, x, R\right)})\\ {\ ({\mathbf{§1}})} \iff & (x > y \to x > y) {\ \land \ }(x \leq y \to x < y)\\ \iff & x \leq y \to x < y \\ \end{split}$

This is not true for all $$x, y \in \mathbb{Z}$$, specifically when $$x = y$$. Therefore: $\begin{split}Q &= x \neq y\\ \end{split}$