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 \left(x+y<z\right)$.
2. $e\models x+y<z\to \neg \left(xy=z\right)$.
3. $e\models y-xz<z$.
4. $e\models \forall u\left(y<u\to yz<uz\right)$.
5. $e\models \forall u\left(u<y\to uz<yz\right)$.
6. $e\models x+y-z<xyz$.

Provas

Exercício 4 Use as regras adequadas para provar:

1. $⊢[[x>0]]\text{y = x + 1}[[y>1]]$.
2. $⊢[[\top ]]\text{y = x; y = x + x + y}[[y=3x]]$.
3. $⊢[[x>1]]\text{P3}[[y>0\wedge 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. $[[\top ]]\text{P}[[y=x+2]]$.
2. $[[\top ]]\text{P}[[z>x+y+4]]$.

Verificação de Programas

Exercício 6 Prove a validade de $$⊢[[\top ]]\text{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 $$⊢[[\top ]]\text{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. $[[\top ]]\text{P}[[w=max(x,y,z)]]$.
2. $[[\top ]]\text{P}[[(x=5\to y=3)\wedge (x=3\to y=-1)]]$.

Exercício 9 A função caraterística da relação $r_n$ é $${\chi }_r(x_1,\dots ,x_n)=\{\begin{array}{ll}1& \text{se}r(x_1,\dots ,x_n),\\ 0& \text{caso contraˊrio.}\end{array}$$

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

Prove a validade de $$⊢[[\top ]]\text{Xpos}[[y={\chi }_{\text{pos}}(x)]]$$ onde Xpos é o programa

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

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

Exercício 10 Prove a validade de $$⊢[[x>0]]\text{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 $$⊢[[y\ge 0]]\text{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 $$⊢[[y=y_0\wedge y\ge 0]]\text{Multi2}[[z=x{y}_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 $$⊢[[x\ge 0]]\text{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 $$⊢[[y\ne 0]]\text{Div}[[x=yd+r\wedge 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 $$⊢[[x\ge 0\wedge y\ge 0]]\text{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: $${⊢}_{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 $$⊢[[x\ge 0]]\text{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 $$⊢[[x\ge 0]]\text{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 $$⊢[[x_0>=0\wedge x=x_0]]\text{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.