(versão de 11 de Fevereiro de 2019)
Verifique a correcção das asserções seguintes, recorrendo ao cálculo de Hoare. Assume-se que variáveis $N$, $X$, e $Y$ denotam números inteiros e que a variável $W$ denota um tuplo de números inteiros.
1.
$\{n == N \,{\tt and }\, N \geq 0\}$ i = n; r = 1 $\{r == \Pi_{k=i+1}^{N} k \,{\tt and }\, i\geq 0\}$
2. $\{x == X \,{\tt and }\, y == Y \}$ z = 1; w = y $\{z == X^{(Y-y)} \,{\tt and }\, w == Y\}$
3. $\{$ True $\}$ a = w; r = 0 $\{{\tt len}(w) == r + {\tt len}(a)\}$
4. $\{$ True $\}$ a = w; r = 0 $\{r == \sum_{k=0}^{{\tt len}(w)-{\tt len}(a)-1}w[k]\,{\tt and }\,
a == w[{\tt len}(w)-{\tt len}(a):]\}$
Verifique a correcção das asserções seguintes, recorrendo ao cálculo de Hoare. Assume-se que variáveis $N$, $X$, e $Y$ denotam números inteiros e que a variável $W$ denota um tuplo de números inteiros.
1. $(i\leq0 \;{\tt and }\; r == \Pi_{k=i+1}^{N} k \;{\tt and }\; i\geq0)\Rightarrow (r == \Pi_{k=1}^{N} k )$
2. $(y==0 \;{\tt and }\; z == X^{(Y-y)} \;{\tt and }\; w==Y)\Rightarrow(z == X^Y \;{\tt and }\; w == Y)$
3. $(a == [] \;{\tt and }\; {\tt len}(w) == r + {\tt len}(a))\Rightarrow(r == {\tt len}(w))$
4. $(a == [] \;{\tt and }\; r == \sum_{k=0}^{{\tt len}(w)-{\tt len}(a)-1}w[k]\;{\tt and }\; a == w[{\tt len}(w)-{\tt len}(a):])\Rightarrow (r == \sum_{k=0}^{{\tt len}(w)-1}w[k])$
Verifique que as asserções seguintes não são asserções verdadeiras. assume-se que as variáveis $N$, $X$, e $Y$ denotam números inteiros e que a variável $W$ denota um tuplo de números inteiros.
1. $(i\leq0 \;{\tt and }\; r == \Pi_{k=i+1}^{N} k)\Rightarrow (r == \Pi_{k=1}^{N} k )$
Para cada um dos programas seguintes verifique, recorrendo ao cálculo de Hoare, que estão parcialmente correctos faces às condições iniciais (C1) e objectivo (C2) indicadas.
Assume-se que as variáveis $N$, $X$, e $Y$ denotam números inteiros e que a variável $W$ denota um tuplo de números inteiros.
1. Cálculo do factorial
def factorial(n):
i = n
r = 1
while i > 0:
r = r * i
i = i - 1
return r
C1: $n==N \;{\tt and }\; N\geq0$
C2: $r == \Pi_{k=1}^{N} k$
2. Exponenciação
def exp(x,y):
if y >= 0:
z = 1
w = y
while y!=0:
y = y - 1
z = z * x
return z
C1: $x = X \;{\tt and }\; y = Y \;{\tt and }\; Y\geq 0$
C2: $z = X^Y \;{\tt and }\; w == Y \;{\tt and }\; y = Y$
3. Comprimento de um tuplo
def comp(w):
a = w
r = 0
while a != ():
r = r + 1
a = a[1:]
return r
C1: True
C2: $r == {\tt len}(w)$
4. Soma dos elementos de um tuplo
def soma(w):
a = w
r = 0
while a != ():
r = r + a[0]
a = a[1:]
return r
C1: True
C2: $r == \sum_{k=0}^{{\tt len}(w)-1}w[k]$
5. Soma dos elementos em posições pares de um tuplo
def soma_pos_pares(w):
i = 0
r = 0
while i < len(w):
if i%2 == 0:
r = r + w[i]
i = i+1
return r
C1: True
C2: $r == \sum_{k=0}^{\left\lfloor\frac{{\tt len}(w)-1}{2}\right\rfloor}w[2k]$
6. Soma dos elementos pares de um tuplo
def soma_pares(w):
i = 0
r = 0
while i < len(w):
if w[i]%2 == 0:
r = r + w[i]
i = i+1
C1: True
C2: $r == \sum_{k=0}^{{\tt len}(w)-1}w[k]\ {\tt if}\ (w[k]\%2==0)\ {\tt else}\ 0$
7. Inversão de um tuplo
def inverte(w):
i = 0
r = ()
while i < len(w):
r = (w[i],) + r
i = i+1
return r
C1: True
C2: $\bigwedge_{k=0}^{{\tt len}(w)-1} r[{\tt len}(w)-k-1] == w[k]$
8. Máximo de um tuplo não vazio
def max(w):
i = 1
r = w[0]
while i < len(w):
if r < w[i]:
r = w[i]
i = i+1
return r
C1: $w==W \;{\tt and }\; W != []$
C2: $\big(\bigwedge_{k=0}^{{\tt len}(W)-1} r \geq W[k]\big) \wedge
\big(\bigvee_{k=0}^{{\tt len}(W)-1} r == W[k]\big)$
9. Supremo de um tuplo
from math import inf
def sup(w):
aux = w
r = -inf
while aux != ():
if r < aux[0]:
r = aux[0]
aux = aux[1:]
return r
C1: True
C2: $r == \sup(w)$
10. Pesquisa de elemento em lista
def pesquisa(x,w):
aux = w
r = False
while aux != ():
r = r or x == aux[0]
aux = aux[1:]
return r
C1: $x==X \;{\tt and }\; w == W$
C2: $r == \big(\bigvee_{k=0}^{{\tt len}(W)-1} X == W[k]\big)$
11. Média dos elementos de um tuplo não vazio
def media(w):
i = 1
r = w[0]
while i < len(w):
r = r + w[i]
i = i+1
r = r/len(w)
return r
C1: $w == W \;{\tt and }\; W != []$
C2: $r = \frac{\sum_{k=0}^{{\tt len}(W)-1} W[k]}{{\tt len}(W)}$
1.
def e1(n):
i = 1
r = 0
while i <= n:
r = r + i
i = i + 1
return r
C1: True
C2: $r == \sum_{k=1}^{n} k$
2.
def e2(w):
i = 0
r = 1
while i < len(w):
r = r * w[i]
i = i + 1
return r
C1: $w != []$
C2: $r == \Pi_{k=0}^{{\tt len}(w)-1} w[k]$
3.
def e3(x, w):
i = -1
r = True
while i < len(w)-1:
i = i +1
r = r and (x == w[i])
return r
C1: $w != []$
C2: $r == \big(\bigwedge_{k=0}^{{\tt len}(w)-1} x == w[k]\big)$
4. Considere o seguinte programa imperativo ${\tt PROG}$
r=0
while x!=1:
r=r+1
x=x/2
Demonstre que é válida a asserção $$ \{{\tt x==2}^{**}{\tt N\}PROG\{r==N\}}. $$
5. Considere o seguinte programa imperativo ${\tt PROG}$
r=0
y=0
while x!=y:
r=r+2*y+1
y=y+1
Demonstre que é válida a asserção $$ \{{\tt True\}PROG\{r==x}^{**}{\tt 2\}}. $$
6. Considere o seguinte programa imperativo ${\tt PROG}$
i=len(w)
r=0
while i!=2:
i=i-1
r=w[i]+x*x
Demonstre que é válida a asserção $$ \{{\tt True\}PROG\{r==}\sum_{\tt 0\leq j<len(w)} {\tt w[j]*x}^{\tt j}{\tt \}}. $$
7. Considere o seguinte programa imperativo ${\tt PROG}$
TBW
Demonstre que é válida a asserção $$ \{{\tt x==2}^{**}{\tt N\}PROG\{r==N\}}. $$
8. Considere o seguinte programa imperativo ${\tt PROG}$
r=0
i=0
s=1
while i!=len(w):
r=r+w[i]
i=i+1
s=-s
Demonstre que é válida a asserção $$ \{{\tt True\}PROG\{r==}\sum_{\tt 0\leq j<len(w)} {\tt (-1)}^{\tt j}{\tt *w[j] \}}. $$
9. Considere o seguinte programa imperativo ${\tt PROG}$
r=[]
a=w[0]
i=1
while i!=len(w):
r=r+[w[i]-a]
a=w[i]
i=i+1
Demonstre que é válida a asserção $$ \{{\tt len(w)>0\}PROG\{w[len(w)-1]==w[0]+}\sum_{\tt x\; in\; r} {\tt x \}}. $$