bc1435 Correção de algoritmos

Um algoritmo (ou programa) está correto se para cada instância do problema que ele resolve, a resposta dada está correta. A prova da correção tem duas partes: provar que a resposta está correta se o programa terminar ( correção parcial ), provar que o programa termina (a complexidade de tempo é um refinamento de uma prova de término). Vejamos uma técnica desenvolvida por Hoare (o mesmo que inventou o Quicksort) para correção parcial de algoritmos.

A seguir, ${p}$ e ${q}$ são proposições.

Definição 1 Um algoritmo, ou trecho de algoritmo, ${S}$ está parcialmente correto com respeito a pré-condição ${p}$ e a pós-condição ${q}$ se sempre que ${p}$ for verdadeiro para os valores de entrada de ${S}$ e ${S}$ terminar, então ${q}$ é verdadeiro para os valores de saída de ${S}$ .

Notação ${p\{S\}q}$ significa ${S}$ está parcialmente correto com respeito a pré-condição ${p}$ e a pós-condição ${q}$ .

Exemplo Por exemplo, se ${p}$ é ${x=1}$ e ${q}$ é ${z=3}$ e ${S}$ é o trecho de programa

 y:=2; z:= x + y;

então, ${p\{S\}q}$ . De fato, suponha ${p}$ . Após a execução de ${S}$ , ${y=2}$ e ${z=1+2}$ pois de ${p}$ temos ${x=1}$ . Portanto, ${z=3}$ .

Regras de Inferência para correção parcial de programas:

1. Composição

$\displaystyle \begin{array}{rcl} &p\{S_1\}q& \\ &q\{S_2\}r& \\ &\textrm{---------}&\\&p\{S_1;S_2\}r&\end{array}$

2. Condicional

2.1. No caso

 Se (condição) então S;

o argumento é

$\displaystyle \begin{array}{rcl} & ( p{~\mathrm{ e }~} \textrm{condi\c c\~ao}) \{S\}q & \\& ( p{~\mathrm{ e }~} \mathrm{n\tilde{a}o}(\textrm{condi\c c\~ao})) \Rightarrow q & \\ &\textrm{---------------------------------}& \\ & p\{ \textrm{Se (condi\c c\~ao) ent\~ao S}\}q& \end{array}$

2.2. No caso

 Se (condição) então S1; senão S2

o argumento é

$\displaystyle \begin{array}{rcl} & ( p{~\mathrm{ e }~} \textrm{condi\c c\~ao}) \{S_1\}q & \\& ( p{~\mathrm{ e }~} \mathrm{n\tilde{a}o}(\textrm{condi\c c\~ao})) \{S_2\} q & \\ &\textrm{------------------------------------------}& \\ & p\{ \textrm{Se (condi\c c\~ao) ent\~ao } S_1 \textrm{ sen\~ao } S_2\}q& \end{array}$

3. Laços No caso

 Enquanto (condição) S;

Nesse caso, $S$ é executado entuanto a condição for verdadeira; devemos escolher uma proposição $p$ que permaneça válida durante as execuçãoes de $S$ . O argumento é

$\displaystyle \begin{array}{rcl} &( p{~\mathrm{ e }~} \textrm{condi\c c\~ao}) \{S\}p &\\ & \textrm{---------------------------------}&\\ &p\{ \textrm{Enquanto (condi\c c\~ao) S}\}(\mathrm{n\tilde{a}o}(\textrm{condi\c c\~ao}){~\mathrm{ e }~} p)& \end{array}$

A proposição ${p }$ é o invariante do laço. Provar que uma proposição é invariante de laço precisa de indução.

Exemplo. Seja ${S}$ o seguinte algoritmo que recebe dois inteiros $m,n$ e devolve o valor da variável produto. Vamos provar que $(m,n\in\mathbb Z)\{S\}(\textrm{produto}=m\cdot n)$

multiplica(m,n:inteiros)
/* Dados : m e n inteiros */
/* Devolve: m n */

/* p: m e n inteiros */

     se (n<0) então a:=-n;
     senão a:=n; 

/* q: p e a=|n| */

     k:=0;
     x:=0;

/* r: q e k=0 e x=0 */

     enquanto (k <= a) */

     {     x:=x+m;
           k:=k+1;
     }

/* s: x=ma e a=|n| */

     se (n<0) então produto:=-x;
              senão produto:=x.

/* t: produto=mn */

A estratégia para provar a correção desse algoritmo é:

${p\{\texttt{se (n<0) ent\~ao a:=-n; sen\~ao a:=n}\}q}$ ;
${q\{\texttt{k:=0; x:=0}\}r}$ ;
${r\{\texttt{enquanto (k<a) \{x:=x+m;k:=k+1; \}}\}s}$ ;
${s\{\texttt{se (n<0) ent\~ao produto:=-x;sen\~ao produto:=x}\}t}$ ;

De 1 e 2 temos

$\displaystyle p \{\texttt{se (n<0) ent\~ao a:=-n; sen\~ao a:=n};\texttt{ k:=0; x:=0}\} r. \ \ \ \ \ (56)$

pela regra da composição. De 3 e 4 temos, por composição novamente

$\displaystyle \begin{array}{rcl} &r \{ \texttt{enquanto (k<0) ent\~ao produto:=-x;} \\ & \texttt{sen\~ao produto:=x}\} t. \end{array}$

que junto com (56), mais a regra da composição resulta que

$\displaystyle (m\in {\mathbb Z} {~\mathrm{ e }~} n\in{\mathbb Z}) \{S\} (produto=mn).$

Agora, vamos provar 1,2,3,4 listados acima.

Sejam ${p\colon m\in{\mathbb Z} {~\mathrm{ e }~} n\in{\mathbb Z}}$ e ${q\colon p {~\mathrm{ e }~} a=|n|}$ as proposições dadas no algoritmo, seja ${R}$ o trecho de programa

$\displaystyle R\colon \texttt{se (n<0) ent\~ao a:=-n; sen\~ao a:=n}.$

Vamos provar

$\displaystyle p \{R\} (a=|n|). \ \ \ \ \ (52)$

Assuma ${m\in{\mathbb Z}}$ e ${n\in{\mathbb Z}}$ .

Se ${m\in{\mathbb Z}}$ e ${n\in{\mathbb Z}}$ e ${n<0}$ então após ${R}$ terminar temos ${a=-n}$ . Se ${n<0}$ então ${|n|=-n}$ portanto ${a=|n|}$ , portanto

$\displaystyle (m\in{\mathbb Z} {~\mathrm{ e }~} n\in{\mathbb Z} {~\mathrm{ e }~} n<0)\{R\}(a=|n|). \ \ \ \ \ (53)$

Agora, se ${m\in{\mathbb Z}}$ e ${n\in{\mathbb Z}}$ e ${\mathrm{n\tilde{a}o}(n<0)}$ então após ${R}$ terminar temos ${a=n}$ . Se ${\mathrm{n\tilde{a}o}(n<0)}$ então ${|n|=n}$ portanto ${a=|n|}$ . Portanto,

$\displaystyle (m\in{\mathbb Z} {~\mathrm{ e }~} n\in{\mathbb Z} {~\mathrm{ e }~} \mathrm{n\tilde{a}o}(n<0))\{R\}(a=|n|). \ \ \ \ \ (54)$

Portanto, de (53), (54) e do argumento 2.2 temos (52), e, portanto, ${p\{R\}q}$ . Agora, considere o trecho

$\displaystyle T\colon \texttt{k:=0;x:=0}$

e vamos provar ${(p {~\mathrm{ e }~} a=|n|)\{T\}(q {~\mathrm{ e }~} k=0 {~\mathrm{ e }~} x=0)}$ .

Após ${\{\texttt{k:=0;x:=0}\}}$ vale ${k=0{~\mathrm{ e }~} x=0}$ , portanto

$\displaystyle q \{\texttt{k:=0;x:=0}\} (q {~\mathrm{ e }~} k=0{~\mathrm{ e }~} x=0) \ \ \ \ \ (55)$

para qualquer proposição verdadeira ${q}$ , em particular quando

$\displaystyle q\colon m\in{\mathbb Z}{~\mathrm{ e }~} n\in{\mathbb Z} {~\mathrm{ e }~} a=|n|$

é verdadeira.

Assuma ${r\colon q {~\mathrm{ e }~} k=0{~\mathrm{ e }~} x=0}$ . Se ${k < a}$ (condição do laço) então o invariante

$\displaystyle x=mk {~\mathrm{ e }~} k\leq a$

é verdadeiro antes da primeira rodada do laço pois ${0=m0 {~\mathrm{ e }~} 0\leq |n|}$ . Assuma $x=mk ~e ~k\leq a ~e~k<a$ antes de uma execução do trecho

$\displaystyle U\colon \texttt{x:=x+m; k:=k+1;}$

Considere uma execução de ${U}$ e denote por ${x'}$ e ${k'}$ os valores das variáveis ${x}$ e ${k}$ antes dessa execução. Então, por hipótese

$\displaystyle x'=mk' {~\mathrm{ e }~} k'\leq a$

e (condição) ${k' < a}$ ; após a execução temos $x=x'+m$ e ${k=k'+1}$ .

Se ${x=x'+m}$ e ${x'=mk'}$ , então ${x=(mk')+m = m(k'+1)}$ .

Se ${k=k'+1}$ ${x= m(k'+1)}$ então ${x=mk}$ .

Se ${k' < a }$ então ${k'+1 \leq a}$ .

Portanto, após a execução de ${U}$ o invariante é verdadeiro, ou seja, “provamos”

$\displaystyle ( x=mk {~\mathrm{ e }~} k\leq a {~\mathrm{ e }~} k <a)\{U\}(x=mk ~e~k\leq a)$

e da regra de inferência para laços, temos

$\displaystyle ( x=mk {~\mathrm{ e }~} k\leq a) \{\texttt{enquanto (k<a) U}\}(\mathrm{n\tilde{a}o}(k<a)~e~x=mk{~\mathrm{ e }~} k\leq a )$

ainda, ${(\mathrm{n\tilde{a}o}(k < a)~e~x=mk{~\mathrm{ e }~} k\leq a )\equiv( x=ma)}$ . Portanto,

$\displaystyle r \{\texttt{enquanto (k<a) U}\}(x=ma)$

logo ${r \{\texttt{enquanto (k<a) U} \}s}$ , onde ${s\colon x=ma {~\mathrm{ e }~} a=|n|}$ .

Finalmente, assuma ${s}$ , denote por ${Q}$ o trecho de programa ${\texttt{se (n<0) ent\~ao produto:=-x; sen\~ao produto:=x}}$ e vamos provar ${t\colon produto=mn}$ .

Se ${s}$ , então ${x=m|n|}$ .

Se ${x=m|n|}$ e ${n<0}$ então após ${Q}$ , ${produto=-x}$ .

Se ${produto=-x}$ e ${x=m|n|}$ e ${n<0}$ então ${produto = -m|n| = -m(-n) = mn}$ . Portanto ${t}$ .

Agora, se ${x=ma}$ e ${a=|n|}$ , então ${x=m|n|}$ .

Se ${x=m|n|}$ e ${\mathrm{n\tilde{a}o}(n<0)}$ então após ${Q}$ , ${produto=x}$ .

Se ${produto=x}$ e ${x=m|n|}$ e ${\mathrm{n\tilde{a}o}(n<0)}$ então ${produto = m|n| = mn}$ . Portanto, pelo argumento 2.2 para condicionais

$\displaystyle (x=ma {~\mathrm{ e }~} a=|n|)\{Q\}(produto=mn).$

Mais invariante de laço.

Consideremos o seguinte algoritmo:

fat(n)
/* Dados : n natural */
/* Devolve: n !*/

i:=1;
f:=1;
enquanto (i < n) {
	 f := f*(i+1);
         i := i+1;}
devolva f.

Vamos provar que a seguinte proposição é um invariante do laço na terceira linha do algoritmo

$\displaystyle i \geq 1 {~\mathrm{ e }~} i \leq n {~\mathrm{ e }~} f = i! \ \ \ \ \ (58)$

Antes, porém, notemos que o invariante e a negação da condição do laço resulta que quando o laço termina temos ${i \geq 1}$ e ${i \leq n}$ e ${f = i!}$ e ${\mathrm{n\tilde{a}o}(i <n)}$ , ou seja, $i=n$ e $f=n!$ , provando a correção parcial.

Vamos provar que a proposição (58) é verdadeira independente do número de vezes que o laço é executado. A prova é por indução no número de iterações do ${\texttt{enquanto}}$ .

Suponhamos que a condição do laço vale, ou seja, ${i < n}$ . Antes da primeira iteração (58) é verdadeiro pois ${i=f=1!=1}$ .

Suponhamos que $i<n$ e que ${ i \geq 1 {~\mathrm{ e }~} i \leq n {~\mathrm{ e }~} f = i! }$ . Após a execução de $\mathtt{ f := f*(i+1)}$ e após a execução de $\mathtt{ i := i+1;}$ temos que para o novo valor de ${i}$ , ${i\geq 1}$ e ${i \leq n}$ e ${f = i!}$ .

Exemplo.
Prove que o seguinte programa está parcialmente correto.

Divisão_inteira(a,d) 

  /* Dados : a natural e d natural positivo */
  /* Devove : inteiros q  e r tais que a=dq+r e 0   r < d */

1.  r := a;
2.  q := 0;
3.  enquanto (r   d)
4.    { r := r-d;
5.      q := q+1; }
6. devolva q,r.

Prova: Sejam ${R}$ o trecho de programa definido pelas linhas 1 e 2, ${S}$ o trecho de programa definido pelas linhas 3 — 5, ${T}$ todo o programa, e ${p}$ e ${t}$ as proposições:

$\displaystyle \begin{array}{rcl} p&\colon& a\in{\mathbb N}{~\mathrm{ e }~} d\in{\mathbb N}\setminus\{0\};\\ t&\colon& q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} a=dq+r {~\mathrm{ e }~} 0\leq r < d\end{array}$

É imediato que

$\displaystyle p\{R\}(q\in{\mathbb Z}{~\mathrm{ e }~} r\in{\mathbb Z}{~\mathrm{ e }~} r=a{~\mathrm{ e }~} q=0). \ \ \ \ \ (59)$

Portanto,

$\displaystyle p\{R\}(q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} a=dq+r{~\mathrm{ e }~} 0\leq r).$

Assumindo

$\displaystyle u\colon q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} r\geq 0{~\mathrm{ e }~} a=dq+r$

como invariante do laço de ${S}$ , temos, já que ${(r\not\geq d)}$ é a condição de parada do laço, que

$\displaystyle (q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} a=dq+r{~\mathrm{ e }~} 0\leq r)\{S\} (q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} r\geq 0{~\mathrm{ e }~} a=dq+r{~\mathrm{ e }~} r\not\geq d).$

Logo,

$\displaystyle p\{R;S\}(q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} a=dq+r{~\mathrm{ e }~} 0\leq r <d)$

e, dessarte, ${p\{T\}t}$ .

Resta-nos ainda mostrar ${u}$ serve como invariante do laço definido por ${S}$ . Como ${r\geq 0{~\mathrm{ e }~} a=dq+r}$ se ${r=a}$ e ${q=0}$ , temos, da asserção 59, que ${p\{R\}u}$ . Analisemos agora o que acontece quando executamos ${\mathtt{\{r := r-d; q := q+1\}}}$ assumindo as 4 e 5: sendo ${r'}$ e ${d'}$ os novos valores de, respectivamente, ${r}$ e ${d}$ , verificamos que ${q'=q+1}$ e ${r'=r-d}$ . Consequentemente, já que ${r\geq d}$ , ${r'\geq 0}$ ,

$\displaystyle dq'+r' = d(q+1)+(r-d) = dq+r = a,$

e, finalmente,

$\displaystyle p\{R\}(u{~\mathrm{ e }~} r\geq d)\mathtt{\{r := r-d; q:= q+1\}}(q\in{\mathbb Z} {~\mathrm{ e }~} r\in{\mathbb Z} {~\mathrm{ e }~} r\geq 0{~\mathrm{ e }~} a=dq+r).$

o que prova que ${u}$ é de fato um invariante para o laço definido por ${S}$ . $\Box$

Algoritmos recursivos.

Exemplo

 fat(n)
/* Dados : n natural */
/* Devolve: n !*/

se (n=0) fat:=1;
 senão fat:= n*fat(n-1);
devolva fat.

A prova da correção é fácil usando indução que $(n\in\mathbb{N})\{\texttt{fat(n)}\}(\texttt{fat}=n!)$ .

Assuma $n\in\mathbb N$

se $n=0$ então após $\textrm{fat:=1}$ temos $\textrm{fat}=1$ , portanto se $n=0$ então $\textrm{fat} =0!$ ; assuma que se $n> 0$ então $\textrm{fat}(n-1) = (n-1)!$
se $\textrm{n\~ao}(n=0)$ então $n>0$ pois $n\in\mathbb{N}$ , como não vale a condição temos $\texttt{fat:=n*fat(n-1)}$ , portanto, pela hipótese da indução, após a execução do código temos $\textrm{fat} =n\cdot(n-1)! = n!$

pela regra de inferência 2.2, $(n\in\mathbb N)\{\texttt{se (n=0) fat:=1; senao fat:=n*fat(n-1)}\}(\textrm{fat}=n!)$ .

Exercício. Prove a correção de

pot(a,n)
/* Dados : a real positivo e n natural */
/* Devolve: a^n */

 se (n=0) pot:=1;
  senão pot:= a*pot(a,n-1);
 devolva pot.

Notas de aula

Jair Donadelli

bc1435 Correção de algoritmos

Deixe um comentário Cancelar resposta

Compartilhe isso:

Relacionado

Deixe um comentário Cancelar resposta