ROUGH DRAFT authorea.com/14409
Main Data History
Export
Show Index Toggle 0 comments
  •  Quick Edit
  • 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.

    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}\]

    Ex3.b

    Given: \[\begin{split} Q &: {\varnothing}= {{\mathbf{\top}}}\\ R &: res = n_0m_0\\ I &: (res + nm = n_0m_0) {\ \land \ }(n \geq 0)\\ B &: 0 < n\\ V &: n\\ S &: \{ res, n := res + m, n - 1 \} \end{split}\]

    I holds immediately before loop

    We are proving that: \(Q \to {wp\left(S_1, I\right)}\), where \(S_1\) is the statement before the loop. \[\begin{split} & S_1 &=& S_{11}; S_{12}\\ & S_{11} &=& res := 0\\ & S_{12} &=& {{if\left(n_0 \geq 0\right) \ \{ n, m := n_0, m_0 \}} \ {else \ \{ n, m := -n_0, -m_0 \}}}\\ & Q &\to& {wp\left(S_1, I\right)}\\ \iff & Q &\to& {wp\left(S_{11}; S_{12}, I\right)}\\ {\ ({\mathbf{§2}})} \iff & Q &\to& {wp\left(S_{11}, {wp\left(S_{12}, I\right)}\right)}\\ {\ ({\mathbf{§3}})} \iff & Q &\to& {wp\left(res := 0, (n_0 > 0 \to {wp\left(n, m := n_0, m_0, I\right)}) {\ \land \ }\\ (n_0 \leq 0 \to {wp\left(n, m := -n_0, -m_0, I\right)})\right)}\\ {\ ({\mathbf{§1}})} \iff & Q &\to& {wp\left(res := 0, (n_0 > 0 \to (res + n_0m_0 = n_0m_0) {\ \land \ }n_0 \geq 0) {\ \land \ }\\ (n_0 \leq 0 \to (res + n_0m_0 = n_0m_0) {\ \land \ }-n_0 \geq 0)\right)}\\ {\ ({\mathbf{§1}})} \iff & Q &\to& (n_0 > 0 \to (n_0m_0 = n_0m_0) {\ \land \ }n_0 \geq 0) {\ \land \ }\\ & & & (n_0 \leq 0 \to (n_0m_0 = n_0m_0) {\ \land \ }-n_0 \geq 0)\\ \iff & Q &\to& (n_0 > 0 \to n_0 \geq 0) {\ \land \ }(n_0 \leq 0 \to -n_0 \geq 0)\\ \iff & Q &\implies & {{\mathbf{\top}}}\end{split}\]