Software Specification Exercises: Hoare Logic

Software Specification, MEIC @ IST, 2019/20

jff

## Instructions - You can use the arrow keys, PgDown and PgUp to browse these exercises - You can use Escape to see an overview - You can use Ctrl+Click to zoom in

## Verifying Simple Programs The goal of today's session is to practice the rules of Hoare Logic. Prove each of the following triples twice: first, by writing a derivation tree; second, by decorating them. Suggestion: revise the material discussed in [Lecture 2](02-hoare.html) and [Lecture 3](03-hoare-cont.html).

1. Three-variable swap

$$ \scriptsize \begin{array}{l} \{ x=m \wedge y=n \}\\ t := x; \\ x := y; \\ y := t \\ \{ x=n \wedge y=m \} \end{array} $$

2. Two-variable swap

$$ \scriptsize \begin{array}{l} \{ x=m \wedge y=n \}\\ x := x+y; \\ y := x-y; \\ x := x-y \\ \{ x=n \wedge y=m \} \end{array} $$

3. Maintaining a property

$$ \scriptsize \begin{array}{l} \{ x = r + (y\times q) \}\\ r := r-y; \\ q := q+1 \\ \{ x = r + (y\times q) \}\\ \end{array} $$

4. The maximum value

$$ \scriptsize \begin{array}{l} \{\,\,true\,\,\} \\ \texttt{if}\,\,\,x\ge y\,\,\,\texttt{then} \\ ~~~~~~ m := x \\ \texttt{else} \\ ~~~~~~ m := y \\ \{\,\,m = max(x, y)\,\,\} \end{array} $$

Assume that for all $x$ and $y$ we have $x\ge y \rightarrow max(x,y)=x$

5. Adding one to the other

$$ \scriptsize \begin{array}{l} \{ x=m \wedge y=n \wedge 0\leq n \}\\ \texttt{while}\,\,0\lt y\,\,\texttt{do \{} \\ ~~~ x := x+1; \\ ~~~ y := y-1 \\ \texttt{\}}\\ \{ x = m+n \} \end{array} $$

6. Integer division

$$ \scriptsize \begin{array}{l} \{ A\gt 0 \wedge B\gt 0 \}\\ q := 0; \\ r := A; \\ \texttt{while}\,\,r\ge B\,\,\texttt{do \{} \\ ~~~ q := q+1; \\ ~~~ r := r-B \\ \texttt{\}}\\ \{ A = q\times B + r \,\,\wedge\,\, 0\le r \,\,\wedge\,\, r\lt B \} \end{array} $$

7. Factorial

$$ \scriptsize \begin{array}{l} \{ x \ge 0 \}\\ y := 1; \\ z := 0; \\ \texttt{while}\,\,z\neq x\,\,\texttt{do \{} \\ ~~~ z := z+1; \\ ~~~ y := y*z \\ \texttt{\}}\\ \{ z = x \,\wedge\, y=x! \} \end{array} $$

8. Euclid's algorithm

$$ \scriptsize \begin{array}{l} \{ 0\lt M \,\wedge\, 0\lt N\}\\ x:=M;\,\,y:=N;\\ \texttt{while}\,\,x\neq y\,\,\texttt{do \{} \\ ~~~ \texttt{if}\,\,\,x\lt y\,\,\,\texttt{then} \\ ~~~~~~~~~ y := y-x \\ ~~~ \texttt{else} \\ ~~~~~~~~~ x := x-y \\ \texttt{\}}\\ \{ x = y = GCD(M,N) \} \end{array} $$

9. Exponentiation

$$ \scriptsize \begin{array}{l} \{ A\ge 0 \,\wedge\, B\ge 0\}\\ r:=1;\,\,x:=0;\\ \texttt{while}\,\,x\neq B\,\,\texttt{do \{} \\ ~~~~~~ r := r*A; \\ ~~~~~~ x := x+1 \\ \texttt{\}}\\ \{ r = A^B \} \end{array} $$