Exercícios de Verificação de Programas

Estes exercícios foram copiados e/ou inspirados nas seguintes obras:

• Lógica e Aritmética de Augusto Franco de Oliveira.
• forallχ de P. D. Magnus.
• Logic in Computer Science de Michael Huth e Mark Ryan.
• Artificial Intelligence, A Modern Approach de Stuart Russell e Peter Norvig.
• Mathematics for Computer Science: Course Textbook de Eric Lehman, F Thomson Leighton e Albert R Meyer.

Instruções Extra

Exercício 1 Em que circunstâncias a instrução if G {A} else {B} não termina?

Exercício 2 Uma instrução comum que não está presente na nossa linguagem de programação é o for, que pode ser usado para somar termos de uma sucessão como no exemplo seguinte:

#![allow(unused)]
fn main() {
s = 0;
for i = 0; i <= max; i = i + 1 {
    s = s + 2 * i;
} 
}

Depois de executar a cópia s = 0 inicial, a instrução for executa primeiro i = 0, depois o corpo s = s + 2 * i seguido do incremento i = i + 1 repetidamente até que i <= max fique falso.

Explique como a instrução for pode ser definida na linguagem inicial.

Estado

Exercício 3 Para cada estado $e$ tal que $v_e(x) = -2, v_e(y) = 5$ e $v_e(z) = -1$, determine, justificando, quais da seguintes relações são válidas:

1. $e \models \neg\del{x + y < z}$.
2. $e \models x + y < z \to \neg\del{xy = z}$.
3. $e \models y - xz < z$.
4. $e \models \forall u \del{y < u \to yz < uz}$.
5. $e \models \forall u \del{u < y \to uz < yz}$.
6. $e \models x + y - z < xyz$.

Provas

Exercício 4 Use as regras adequadas para provar:

1. $\vdash \hoare{x > 0}{y = x + 1}{y > 1}$.
2. $\vdash \hoare{\top}{y = x; y = x + x + y}{y = 3x}$.
3. $\vdash \hoare{x > 1}{P3}{y > 0 \land x > y}$ onde P3 é

#![allow(unused)]
fn main() {
a = 1;
y = x;
y = y - a;
}

Exercício 5 Escreva programas tais que os triplos seguintes sejam válidos e, de seguida, faça as respetivas demonstrações.

1. $\hoare{\top}{P}{y = x + 2}$.
2. $\hoare{\top}{P}{z > x + y + 4}$.

Verificação de Programas

Exercício 6 Prove a validade de $$ \vdash \hoare{\top}{P}{z = \min(x,y)} $$ onde $\min(x,y)$ é o menor de $x$ e $y$ e P é o programa

#![allow(unused)]
fn main() {
if x > y {
    z = y;
} else {
    z = x;
}
}

Exercício 7 Prove a validade de $$ \vdash \hoare{\top}{P}{z = \min(x,y)} $$ onde $\min(x,y)$ é o menor de $x$ e $y$ e P é o programa

#![allow(unused)]
fn main() {
if x <= y {
    z = x;
} else {
    z = y;
}
}

Exercício 8 Para cada uma das especificações seguintes escreva um programa adequado e prove que está correto:

1. $\hoare{\top}{P}{w = \max(x, y, z)}$.
2. $\hoare{\top}{P}{(x = 5 \to y = 3) \land (x = 3 \to y = -1)}$.

Exercício 9 A função caraterística da relação $r_n$ é $$ \chi_r(x_1, \ldots, x_n) = \begin{cases} 1&\text{se}~r(x_1, \ldots, x_n), \ 0&\text{caso contrário.} \end{cases}$$

Por exemplo, $\chi_{\text{par}}(2) = 1$ e $\chi_{\text{maior}}(2, 3) = 0$.

Prove a validade de $$ \vdash \hoare{\top}{Xpos}{y = \chi_{\text{pos}}(x)} $$ onde Xpos é o programa

#![allow(unused)]
fn main() {
if x > 0 {
    y = 1;
} else {
    y = 0;
}
}

e $$ \forall x~\text{pos}(x) \leftrightarrow x > 0. $$

Exercício 10 Prove a validade de $$ \vdash \hoare{x > 0}{Copy1}{x = y} $$ onde Copy1 é o programa

#![allow(unused)]
fn main() {
a = x;
y = 0;
while a != 0 {
    y = y + 1;
    a = a - 1;
}
}

Exercício 11 Prove a validade de $$ \vdash \hoare{y \geq 0}{Multi1}{z = xy}$$ onde Multi1 é o programa

#![allow(unused)]
fn main() {
a = 0;
z = 0;
while a != y {
    z = z + x;
    a = a + 1;
}
}

Exercício 12 Prove a validade de $$ \vdash \hoare{y = y_0 \land y \geq 0}{Multi2}{z = xy_0}$$ onde Multi2 é o programa

#![allow(unused)]
fn main() {
z = 0;
while y != 0 {
    z = z + x;
    y = y - 1;
}
}

Exercício 13 Prove a validade de $$ \vdash \hoare{x \geq 0}{Copy2}{y = x}$$ onde Copy2 é o programa

#![allow(unused)]
fn main() {
y = 0;
while y != x {
    y = y + 1;
}
}

Exercício 14 É suposto o programa Div calcular o dividendo dos inteiros $x$ e $y$; isto é, o único inteiro $d$ tal que existe um inteiro $r$ (o resto) tal que $r < y$ e $x = yd + r$.

Por exemplo, se $x = 15$ e $y= 6$ então $d = 2$ porque $x = 6\times 2 + 3$, com $r = 3 < 6$.

Prove que $$ \vdash \hoare{y \not= 0}{Div}{x = y d + r \land r < y} $$ sendo Div o programa

#![allow(unused)]
fn main() {
r = x;
d = 0;
while r >= y {
    r = r - y;
    d = d + 1;
}  
}

Exercício 15 Prove a validade de $$ \vdash \hoare{x \geq 0 \land y \geq 0}{Minup}{z = \min(x,y)} $$ onde $\min(x,y)$ é o menor de $x$ e $y$ e Minup é o programa

#![allow(unused)]
fn main() {
z = 0;
while z < y and z < x {
    z = z + 1;
} 
}

Exercício 16 Modifique o exercício anterior de forma a calcular o máximo de $x,y$. Use a seguinte igualdade aritmética: $$\vdash_{AR} \max(x,y) = x + y - \min(x, y) $$

Exercício 17 Complete o programa seguinte, e demonstre a sua validade, de forma a calcular o máximo de $x,y$.

#![allow(unused)]
fn main() {
? ? x;
while ? ? y {
    z = z + 1;
} 
}

Exercício 18 Prove a validade de $$ \vdash \hoare{x \geq 0}{Downfac}{y = x!} $$ onde Downfac é o programa

#![allow(unused)]
fn main() {
a = x;
y = 1;
while a > 0 {
    y = y * a;
    a = a - 1;
}
}

Exercício 19 Prove a validade de $$ \vdash \hoare{x \geq 0}{Somat1}{y = \frac{x (x + 1)}{2}} $$ onde Somat1 é o programa

#![allow(unused)]
fn main() {
i = 0;
y = 0;
while i <= x {
    i = i + 1;
    y = y + i;
}
}

sabendo que $$ 1 + \cdots + n = \frac{n (n + 1)}{2} $$

Exercício 20 Prove a validade de $$ \vdash \hoare{x_0 >= 0 \land x = x_0}{Somat2}{y = \frac{x_0 (x_0 + 1)}{2}} $$ onde Somat2 é o programa

#![allow(unused)]
fn main() {
y = 0;
while x > 0 {
    y = y + x;
    x = x - 1;
}
}

usando as igualdades aritméticas do exercício anterior.