Análise e Técnicas de Algoritmos
Período 2003.2

Invariante de Laço

Invariante de Laço

Introdução

O conceito de invariante de laço é bastante importante e pode nos ajudar a analisar programas, verificar erros, e derivar programas a partir de especificações.

O invariante de laço pode ser definido como uma relação entre as variáveis de um algoritmo (programa) que é verdadeira nas seguintes condições:

antes do início do laço;
durante a manutenção do laço;
na saída do laço.

Para ilustrar o conceito de invariante de laço, vamos considerar o seguinte algoritmo que computa a soma dos elementos de um array de inteiros.

$\begin{algorithmic} \par\STATE {\bf int Soma(int A[])} \STATE $s \leftarrow 0$\S... ... + A[i]$ \STATE $i \leftarrow i + 1$\ENDWHILE \STATE return $s$\end{algorithmic}$

É possível identificar invariantes de laço nesse exemplo?

Ainda sobre Laços

Em um laço é possível identificar dois elementos:

Guarda é a expressão booleana que determina se o corpo do laço deve ser executado. O algoritmo executa as instruções do corpo do laço sempre que a guarda é avaliada verdadeira. Em nosso exemplo, a guarda é $i \leq A.length$ .
Variante é a expressão numérica que mede o quanto de execução ainda falta. A variante pode não estar explicitada no algoritmo (quase sempre isso acontece). Em geral, a variante é o número de iterações que ainda resta ocorrer. No nosso exemplo, a variante é .

Um laço está correto se as seguintes 5 condições são satisfeitas:

Início: O invariante é verdadeiro antes de entrar no laço.
Invariância: O corpo do laço preserva o invariante.
Progresso: O corpo do laço diminui a variante.
Limitação: Quando a variante atinge certo valor, a guarda se torna falsa.
Saída: A negação da guarda e o invariante descrevem o objetivo do laço.

Verificar no exemplo se as 5 condições são satisfeitas.

Um outro exemplo

O seguinte algoritmo computa através de multiplicações sucessivas. Determine os invariantes de laço.

$\begin{algorithmic} \par\STATE {\bf int Potencia(int $x$, int $n$)} \STATE $p \l... ...times x$ \STATE $i \leftarrow i + 1$\ENDWHILE \STATE return $p$\end{algorithmic}$

Derivando Laços em um Algoritmo

A partir de invariantes, é possível derivar laços em um algoritmo. Para tanto, vamos considerar um padrão que relaciona as instruções de um laço:

$\begin{algorithmic} \par\STATE $PRE$\STATE $\rhd$\ Invariante é verdadeiro \WHIL... ...ATE $\rhd \neg G \wedge $\ Invariante é verdadeiro \STATE $POS$\end{algorithmic}$

é a guarda do laço, é o código que precede o laço, corresponde ao corpo do laço e é o código que vem depois do laço.

Para ilustrar a derivação de laços, vamos considerar a definição da divisão de inteiros que relaciona as saídas (quociente) e (resto) às entradas (número) e (divisor). Por definição, sabemos que e $n = q \times d + r$ .

De fato, a definição da divisão corresponde a pós-condição do laço (aquilo que é verdade após a execução do laço). Sabemos que na pós-condição, $\rhd \neg G \wedge$ Invariante é verdadeiro. É fácil perceber que $\neg G = r < d$ e o invariante é $n = q \times d + r$ . Logo, a guarda é $r \geq d$ . Substituindo no padrão definido acima temos:

$\begin{algorithmic} \par\STATE $PRE$\STATE $\rhd$\ $n = q \times d + r$\WHILE{$ ... ...\rhd \neg (r \geq d) \wedge $\ $n = q \times d + r$\STATE $POS$\end{algorithmic}$

Devemos derivar ainda e , uma vez que pode ser (return ). A idéia básica é contar quantas vezes nós subtraímos o divisor do numerador . O quociente é o contador e o resto é o que sobra após a subtração. É justo considerar que inicialmente não fizemos nenhuma subtração. É importante ainda lembrar que o invariante deve ser válido antes do laço. Logo, se iniciamos $q \leftarrow 0$ , indicando que não fizemos ainda nenhuma subtração, devemos fazer $r \leftarrow n$ para garantir o invariante.

Para definir o corpo do laço, devemos presevrar o inavariante. Logo, para cada subtração, o contador é incrementado de e o divisor subtraído do resto ( $r \leftarrow r - d$ ).

O algoritmo derivado é, portanto,

$\begin{algorithmic} \par\STATE $r \leftarrow n$\STATE $q \leftarrow 0$\STATE $\r... ...neg ( r \geq d) \wedge $\ $n = q \times d + r$\STATE return $q$\end{algorithmic}$