Below you can find some examples on correctness checking and derivation through calculation of simple programs. These exercises are part of the Formal Methods in Software Engineering course given at the Masters in Informatics Engineering at the Faculty of Engineering, University of Porto.
Find the Weakest Precondition of the following:
1.1. $\{wp\}$ b:=c+1; a:=c+2 $\{c<b ∧ b<a\}$
$wp($b:=c+1, $wp($a:=c+2, $c<b ∧ b<a))$
$≡$ { Successive application of the assignment := rule }
$wp($a:=c+2, $c<b ∧ b<a) → c<b ∧ b<c+2$
$wp($b:=c+1, $c<b ∧ b<c+2) → c<c+1 ∧ c+1<c+2 ≡$ $\text{True}$ .
1.2. $\{wp\}$ if (a>b) then c:=a $\{ c=\text{max}(a,b) \}$
If we assume this definition:
\[\text{max}(a,b) ≜ \begin{cases} a &\mbox{if } a > b \\ b & \mbox{if } a ≤ b \end{cases}\]It follows that:
$wp($if (a>b) then c:=a, $c=\text{max}(a,b))$
$≡$ { By the if rule }
$a>b ∧ wp($c:=a, $c=\text{max}(a,b)) ∨ a≤b ∧ wp($skip, $c=\text{max}(a,b))$
$≡$ { Assignment := and skip rule }
$a>b ∧ a=\text{max}(a,b) ∨ a≤b ∧ c=\text{max}(a,b)$
$≡$ { By the definition of $\text{max}(a,b)$ }
$a>b ∧ a=a ∨ a≤b ∧ c=b$
$≡$ { Identity }
$a>b ∨ a≤b ∧ c=b$
$≡$ { Distributive Property of ∨ }
$(a>b ∨ a≤b) ∧ (a>b ∨ c=b)$
$≡$ { Left identity of ∧, since $(a>b ∨ a≤b)$ is a tautology }
$a>b ∨ c=b$ .
Find if the following triplets hold (i.e., true or false), by calculating the Weakest Precondition:
2.1. $\{y=3\}$ y:=x-y; x:=y+1; y:=x-1 $\{y<x\}$
First we calculate the weakest precondition:
$wp($y:=x-y, $wp($x:=y+1, $wp($y:=x-1, $y < x)))$
$≡$ { Successive application of the assignment := rule }
$wp($y:=x-1, $y<x) → x-1<x$
$wp($x:=y+1, $x-1<x) → y<y+1 ≡ y<y+1$
$wp($y:=x-y, $y<y+1) → x-y < (x-y)+1 ≡ \text{True}$
Now we need to prove that the implication holds:
$(y=3)→\text{True}→\:?→$ $\text{True}$ .
2.2. $\{x≥-100 ∧ x≤100\}$ if (x<0) then x:=x+100 else y:=2*x fi $\{y≥0 ∧ y≤300\}$
First we calculate the weakest precondition:
$wp($if (x<0) then x:=x+100 else y:=2*x fi, $0 ≤ y≤300)$
$≡$ { By the if rule }
$x<0 ∧ wp($x:=x+100, $0≤y≤300) ∨ x≥0 ∧ wp($y:=2*x, $0≤y≤300)$
$≡$ { Assignment := rule }
$x<0 ∧ 0≤y≤300 ∨ x≥0 ∧ 2x≥0 ∧ 2x≤300$
$≡$ { Algebra and set theory }
$x<0 ∧ 0≤y≤300 ∨ 0≤x≤150$
Now we need to prove that the implication holds:
$(x≥-100 ∧ x≤100) → (x<0 ∧ 0≤y≤300 ∨ 0≤x≤150) →\: ? →$$\text{False}$ .
Provide the total proof for the following specification:
$[n≥0 ∧ d>0]$
q:=0; r:=n; while (r>=d) do q:=q+1; r:=r−d od
$[n = q⋅d + r∧0≤r ∧ r<d]$
a. We first choose and invariant:
$\:I ≜ n = q⋅d+r ∧ r≥0 ∧ d>0\:$
b. And a variant:
$\:M ≜ r\:$
c. We provide proof that the invariant holds before the loop:
$[P]$ q:=0; r:=n $[I]$
$≡$ { By the definition of $I$ and $wp$}
$P → wp($q:=0, $wp($r:=n, $n = q ⋅ d + r ∧ r ≥ 0 ∧ d>0$
$≡$ { Successive application of the assignment := rule }
$P → (n = 0 ⋅ d + n ∧ n ≥ 0 ∧ d>0)$
$≡$ { Definition of $P$, algebra and set theory }
$n ≥ 0 ∧ d > 0 → (n = n ∧ n ≥ 0 ∧ d>0) ≡$ $\:\text{True}\:$
d. We provide proof that the invariant holds during the loop and that the variant is strictly decreasing:
$[I ∧ C ∧ M = M’]$ q:=q+1; r:=r-d $[I ∧ M < M’]$
$≡$ { Definition of $I$ and $M$ }
$[\ldots]$ q:=q+1; r:=r-d $[n = q ⋅ d + r ∧ r ≥ 0 ∧ d>0 ∧ r < M’]$
$≡$ { Proof by $wp$ }
$\ldots\: → wp($q:=q+1, $wp($r:=r-d, $n = q ⋅ d + r ∧ r ≥ 0 ∧ d>0 ∧ r < M’))$
$≡$ { Successive application of the assignment := rule }
$\ldots\: → n = (q + 1) ⋅ d + (r - d) ∧ (r-d) ≥ 0 ∧ d>0 ∧ (r - d) < M’$
$≡$ { Definition of $I$, $C$, $M$ and algebra }
$(n = q⋅d + r ∧ r≥0 ∧ r≥d ∧ d>0 ∧ r=M’) → (n = q⋅d + r ∧ (r-d)≥0 ∧ d>0 ∧ (r-d)< M’)$
$≡$ { Algebra and set theory }
$\:\text{True}\:$
e. We provide proof that the post-condition is implied by loop termination:
$I ∧ ¬ C → Q$
$≡$ { Definition of $I$, $C$ and $Q$ }
$(n = q ⋅ d + r ∧ r ≥ 0∧ d>0 ∧ r < d) → (n = q ⋅ d + r ∧ 0 ≤ r ∧ r < d)≡$ $\:\text{True}\:$
f. We provide proof that the variant is strictly positive before the loop:
$I ∧ C → M > 0$
$≡$ { Definition of $I$, $C$ and $M$ }
$(n = q ⋅ d + r ∧ r ≥ 0 ∧ r >= d ∧ d>0) → (r > 0)≡$ $\:\text{True}\:$
Find the program S that refines the following specifications:
4.1. $\{x=0\}$ S $\{y=x\}$
Spec($x=0$, S, $y=x$)
$\sqsubseteq$ { Refinement of the assignment := }
Spec($x=0$, y:=x, $y=x$).
4.2. $\{y=2 ∧ x=3\}$ S $\{x=3\}$
Spec($y=2 ∧ x=3$, S, $x=3$)
$\sqsubseteq$ { Refinement of skip, given that $y=2 ∧ x=3 → x=3$ }
Spec($y=2 ∧ x=3$, skip, $x=3$).
Prove o seguinte programa através de refinamento (indique as regras que aplicou em cada passo).
$\{ x = m ∧ y = n ∧ m>0\}$
while (x!=0) do y:=y-1; x:=x-1 od
$\{ y = n - m \}$
O ponto de partida é então:
Spec($x=m ∧ y=n ∧ m>0$, S, $y=n-m)$
a. Encontrar invariante e variante do ciclo e verificar aplicabilidade da regra da repetição. Lembrando a regra da repetição (para caso de condição de guarda simples, e com $I$ em vez de $P$, considerando que desempenha o papel de invariante do ciclo):
$\{I\}$ S $\{I∧¬G\}$
$\sqsubseteq$ { Regra da repetição }
$\{I\}$ while G do $\{I∧G∧V=V_0\}$ S1 $\{I∧0 ≤ V<V_0\}$ od $\{I∧¬G\}$
Para a aplicar, temos de escolher $I$ (invariante do ciclo) e $V$ (variante do ciclo), e.g.:
$I ≜ y = n-m+x ∧ x≥0$
$V ≜ x$
No entanto, a pré-condição e pós-condição do triplo inicial não são equivalentes a $I$ e $I∧¬G$ (com $G ≜ x≠0$) respectivamente, pelo que temos de começar por enfraquecer a pré-condição e fortalecer a pós-condição, para depois introduzir o ciclo:
$\hphantom{⊑}$ { enfraquecer a pré-condição }
$\{ x = m ∧ y = n ∧ m>0 \}$ S $\{ y = n - m \}$
$⊑$ { dado que $x = m ∧ y = n ∧ m>0 → y = n – m + x ∧ x ≥ 0$ }
$\{ y = n-m+x ∧ x ≥ 0 \}$ S $\{ y = n-m \}$
$⊑$ { fortalecer a pós-condição, dado $(y = n-m+x ∧ x≥0) ∧ ¬x≠0 → y = n-m$ }
$\{\ldots\}$ S $\{ (y = n-m+x ∧ x≥ 0) ∧ ¬x≠0\}$
$⊑$ { introduzir o ciclo, pela regra da repetição, com $V≜x$ }
$\{\ldots\}$ while x!=0 do $\{y=n-m+x ∧ x≥0 ∧ x≠0 ∧ x=V_0\}$ S1 $\{y=n-m+x ∧ x≥0 ∧ 0≤x<V_0\}$ od $\{ (y = n-m+x ∧ x≥0) ∧ ¬x=0\}$
$⊑$ { por simplificação de expressões }
$\{\ldots\}$ while x != 0 do $\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ S1 $\{(y=n-m+x ∧ x≥0 ∧ x<V_0\}$ od $\{ y = n-m+x ∧ x=0 \}$
b. Introduzir sequência aplicando regra da composição. Temos agora que refinar $\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ S1 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$ para $\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ y:=y-1; x:=x-1 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$
Para isso, temos de começar por aplicar a regra da composição, com uma asserção intermédia $M$ apropriada:
$\{y=n-m+x ∧ x>0 ∧ x=V0\}$ S1 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$
$⊑$ { regra da composição }
$\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ S2 $\{M\}$ S3 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$
Uma solução segura é usar a pré-condição mais fraca:
$M ≜ wp($x:=x-1, $y=n-m+x ∧ x≥0 ∧ x<V_0)$
$\hphantom{M} ≡ (y=n-m+x-1 ∧ x-1≥0 ∧ x-1<V_0)$
$\hphantom{M} ≡ (y=n-m+x-1 ∧ x≥1 ∧ x≤V_0)$
c. Introduzir uma das atribuições:
$\{y=n-m+x-1 ∧ x≥1 ∧ x≤V_0\}$ S3 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$
$⊑$ {dado que $(y=n-m+x-1 ∧ x≥1 ∧ x≤V_0) ⇛ (y=n-m+x ∧ x≥0 ∧ x<V_0)[x/x-1]$ }
$\{y=n-m+x-1 ∧ x≥1 ∧ x≤V_0\}$ x: = x-1 $\{y=n-m+x ∧ x≥0 ∧ x<V_0\}$
d. Introduzir a outra atribuição:
$\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ S2 $\{y=n-m+x-1 ∧ x≥1 ∧ x≤V_0\}$
$⊑$ { … }
$\{y=n-m+x ∧ x>0 ∧ x=V_0\}$ y := y-1 $\{y=n-m+x-1 ∧ x≥1 ∧ x≤V_0\}$
Neste caso temos de provar que:
$y=n-m+x ∧ x>0 ∧ x=V_0 ⇛ y-1=n-m+x-1 ∧ x≥1 ∧ x≤V_0$
Ora cada clásula do lado direita é equivalente ou implicada pela cláusula na mesma posição do lado esquerdo, pela que a implicação é sempre verdadeira, para quaisquer valores das variáveis. Isto conclui a prova por refinamento.