Lab3 Report :: Testing Debugging Verification

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.