Resumo da Aula 8

Sumário

Desenvolvimento de ciclos através da metodologia de Dijkstra

1 Desenvolvimento de ciclos através da metodologia de Dijkstra

O desenvolvimento de ciclos é normalmente feito do seguinte modo:

Especificar o problema: definir a pré-condição (PC) e a condição objectivo (CO) do ciclo.
Olhando para a condição objectivo, escolher uma condição invariante (CI) para o ciclo.
Escolher uma guarda (G) tal que CI e ¬G implica CO. Este facto leva a que, se o ciclo terminar, termina num estado em que se verifica a condição objectivo.
Escolher uma inicialização do ciclo (inic) de modo a garantir a veracidade da condição invariante logo no início do ciclo.
Escolher o passo do ciclo de modo a que a condição invariante se mantenha verdadeira (i.e., de modo a garantir que é de facto invariante).
Muito importante: a escolha do passo tem de garantir a terminação do ciclo. O passo é usualmente dividido num progresso (prog) e numa acção (acção), sendo o progresso que garante a terminação do ciclo e a acção que garante que, apesar do progresso, a condição invariante se mantém válida.

1.1 Definição da pré-condição e da condição objectivo

A pré-condição (PC) e a condição objectivo (CO) devem definir de um modo rigoroso e sem ambiguidade quais são os valores permitidos para as variáveis imediatamente antes do início de um troço de código e quais são os valores garantidos para estas variáveis no final desse troço. O troço de código pode corresponder a um ciclo ou ao corpo de uma rotina, por exemplo.

A definição destas condições, no caso de uma rotina, funciona como um contrato estabelecido entre o programador produtor e o programador consumidor da rotina: "desde que o programador consumidor desta rotina a invoque em em circunstâncias em que a pré-condição é verdadeira, o programador produtor desta rotina garante que depois de executada(o) a condição objectivo é verdadeira".

Se se pretender escrever uma função int somaQuadrados(int const n) que some os quadrados dos primeiros n inteiros não-negativos, então a estrutura da função, com a pré-condição e a condição objectivo, poderá ser:

/** Devolve a soma dos primeiros n inteiros não-negativos.
    @pre   (pré-condição da função) 0 <= n.
    @post (condição objectivo da função) somaDosPrimeirosQuadrados = (S k : 0 <= k < n : k²).*/
int somaDosPrimeirosQuadrados(int const n)
{
    // PC (pré-condição do corpo da função): 0 <= n.
    int soma_dos_quadrados =...;

    // CO (condição objectivo do corpo da função):
    //       soma_dos_quadrados = (S k : 0 <= k < n : k²).
    return soma_dos_quadrados;
}

onde CO é a condição objectivo do corpo da função antes da instrução de retorno.

Se se pretender escrever uma função int raizInteiraDe(int const x) que, assumindo que x é não-negativo, devolva o maior inteiro n menor ou igual à raiz quadrada de x, então a estrutura da função, com a pré-condição e a condição objectivo, poderá ser:

/** Devolve a melhor aproximação por defeito da raiz quadrada de x.
    @pre   (pré-condição da função) 0 <= x.
    @post (condição objectivo da função) 0 <= raizInteiraDe <= x^½ < raizInteiraDe + 1,
                           ou seja, 0 <= raizInteiraDe² <= x < (raizInteiraDe + 1)².*/
int raizInteiraDe(int const x)
{
    // PC (pré-condição do corpo da função): 0 <= x.
    int r =...;

    // CO (condição objectivo do corpo da função): 0 <= r² <= x < (r + 1)².
    return r;
}

onde CO é a condição objectivo do corpo da função antes da instrução de retorno. Note-se que é a relação x^½ < raiz + 1 que garante que o valor devolvido é o maior inteiro menor ou igual a x^½.

1.2 Determinação da condição invariante e da guarda

Para encontrar a condição invariante e a guarda dos ciclos utiliza-se normalmente um de dois métodos (ambos constroem a condição invariante por enfraquecimento da condição objectivo):

1.2.1 Substituição de uma constante por uma variável

Muitas vezes é possível obter uma condição invariante para o ciclo substituindo uma constante presente na condição objectivo por uma variável criada para o efeito.

Voltando à função somaDosPrimeirosQuadrados(), é evidente que o corpo da função pode consistir num ciclo cuja condição objectivo já foi apresentada:

CO: soma_dos_quadrados = (S k: 0 <= k < n : k²).

A condição invariante do ciclo pode ser obtida substituindo na condição objectivo CO a constante n por uma variável i, com limites apropriados, ficando portanto

CI: soma_dos_quadrados = (S k: 0 <= k < i : k²) e 0 <= i <= n.

Esta escolha corresponde a relaxar a condição objectivo, pois a condição invariante aceita mais possíveis valores para a variável soma_dos_quadrados do que a condição objectivo, que só aceita o resultado final pretendido. Os valores aceites para essa variável pela condição invariante correspondem a valores intermédios durante o cálculo do valor final. Neste caso correspondem a todas as possíveis somas de quadrados: desde a soma com zero termos até à soma com os n termos pretendidos.

A guarda pode ser obtida facilmente observando que no final do ciclo a guarda será forçosamente falsa e a condição invariante verdadeira (i.e., que CI e ¬G), e que se pretende, nessa altura, que a condição objectivo do ciclo seja verdadeira. Ou seja, sabe-se que no final do ciclo

soma_dos_quadrados = (S k: 0 <= k < i: k²) e 0 <= i <= n e ¬G

e pretende-se que

CO: soma_dos_quadrados = (S k: 0 <= k < n : k²).

A escolha mais simples da guarda que garante a verificação da condição objectivo é

¬G: i = n,
ou seja,
G: i <> n

1.2.2 Factorização da condição objectivo

Quando a condição objectivo é composta pela conjunção de várias condições, pode-se muitas vezes utilizar parte delas como negação da guarda ¬G e a parte restante como condição invariante.

Voltando à função raizInteiraDe(), é evidente que o corpo da função pode consistir num ciclo cuja condição objectivo já foi apresentada:

CO: 0 <= r² <= x < (r + 1)²,

ou seja,

CO: 0 <= r² e r² <= x e x < (r + 1)².

Escolhendo para negação da guarda (¬G) o predicado x < (r + 1)², ou seja, escolhendo

G: (r + 1)² <= x,

obtém-se

CI: 0 <= r² e r² <= x.

Esta escolha faz com que CI e ¬G seja equivalente a CO, pelo que, se o ciclo terminar, termina com o valor correcto.

Esta escolha da condição invariante corresponde a relaxar a condição objectivo, pois a condição invariante aceita mais possíveis valores para a variável r do que a condição objectivo, que só aceita o resultado final pretendido.

1.3 Escolha da inicialização

A inicialização de um ciclo é feita normalmente de modo a, assumindo a veracidade da pré-condição, garantir a verificação da condição invariante da forma mais simples possível.

1.3.1 Função `somaDosPrimeirosQuadrados()`

No caso da função somaDosPrimeirosQuadrados(), a condição invariante é

CI: soma_dos_quadrados = (S k: 0 <= k < i : k²) e 0 <= i <= n,

pelo que a forma mais simples de se inicializar o ciclo é com as instruções

int resultado = 0;
int i = 0;

pois nesse caso a condição invariante fica

CI: 0 = (S k: 0 <= k < 0 : k²) e 0 <= 0 <= n,

que tem sempre valor verdadeiro, pois a pré-condição indica que 0 <= n.

1.3.2 Função `raizInteiraDe()`

No caso da função raiz(), a condição invariante é

CI: 0 <= r² e r² <= x,

pelo que a forma mais simples de se inicializar o ciclo é com a instrução

int r = 0;

pois nesse caso a condição invariante fica

CI: 0 <= 0 e 0 <= x,

que tem sempre valor verdadeiro, pois a pré-condição indica que 0 <= x.

1.4 Determinação do progresso e da acção

A construção de um ciclo fica completa depois de determinado o passo, normalmente constituído pela acção e pelo progresso. O progresso é escolhido de modo a garantir que o ciclo termina, i.e., de modo a garantir que ao fim de um número finito de repetições a guarda se torna falsa. A acção é escolhida de modo a garantir a invariância da condição invariante apesar do progresso, i.e., de modo a garantir que é realizado o que quer que o ciclo deve realizar.

1.4.1 Função `somaDosPrimeirosQuadrados()`

No caso da função somaDosPrimeirosQuadrados(), a guarda é

G: i <> n

pelo que o progresso mais simples é a simples incrementação de i. Ou seja, o passo do ciclo é

// CI e G: soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i <= n e i <> n,
// ou seja,
// soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i < n.
acção
++i; // i = i + 1;
// CI: soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i <= n.

onde se assume a condição invariante como verdadeira no antes da acção e se pretende escolher uma acção de modo a que o seja também depois do passo. Usando a semântica da operação de atribuição, pode-se deduzir a condição mais fraca antes do progresso de modo a que condição invariante seja verdadeira no final do passo:

// soma_dos_quadrados = (S k : 0 <= k < i + 1 : k²) e 0 <= i + 1 <= n,
// ou seja,
// soma_dos_quadrados = (S k : 0 <= k < i + 1 : k²) e -1 <= i < n.
++i; // i = i + 1;
// CI: soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i <= n.

Falta determinar uma acção tal que

// soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i < n.
acção
// soma_dos_quadrados = (S k : 0 <= k < i + 1 : k²) e -1 <= i < n.

A acção mais simples é portanto:

soma_dos_quadrados += i * i;

pelo que o o ciclo (e a função) completo é

/** Devolve a soma dos primeiros n inteiros não-negativos.
    @pre   (pré-condição da função) 0 <= n.
    @post (condição objectivo da função) somaDosPrimeirosQuadrados = (S k : 0 <= k < n : k²).*/
int somaDosPrimeirosQuadrados(int const n)
{
    int soma_dos_quadrados = 0;
    int i = 0;

    // CI: soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i <= n.
    while(i != n) {
        soma_dos_quadrados += i * i;
        ++i;
    }
    return soma_dos_quadrados;
}

ou, substituindo pelo ciclo com a instrução for equivalente:

/** Devolve a soma dos primeiros n inteiros não-negativos.
    @pre   (pré-condição da função) 0 <= n.
    @post (condição objectivo da função) somaDosPrimeirosQuadrados = (S k : 0 <= k < n : k²).*/
int somaDosPrimeirosQuadrados(int const n)
{
    int soma_dos_quadrados = 0;
    int i = 0;

    // CI: soma_dos_quadrados = (S k : 0 <= k < i : k²) e 0 <= i <= n.
    for(int i = 0; i != n; ++i)
        soma_dos_quadrados += i * i;
    return soma_dos_quadrados;
}

1.4.2 Função `raizInteiraDe()`

No caso da função raizInteiraDe(), a guarda é

G: (r + 1)² <= x,

pelo que o progresso mais simples é a simples incrementação de r. Ou seja, o passo do ciclo é

// CI e G: 0 <= r² e r² <= x e (r + 1)² <= x.
acção
++r; // r = r + 1;
// CI: 0 <= r² e r² <= x.

// CI e.G: 0 <= r² e r² <= x e (r + 1)² <= x.
acção
// 0 <= (r + 1)² e (r + 1)² <= x
++r; // r = r + 1;
// CI: 0 <= r² e r² <= x

Como 0 <= r² implica 0 <= (r + 1)², então é evidente que neste caso não é necessária qualquer acção! Assim, o ciclo (a função) completo é:

/** Devolve a melhor aproximação por defeito da raiz quadrada de x.
    @pre   (pré-condição da função) 0 <= x.
    @post (condição objectivo da função) 0 <= raizInteiraDe <= x^½ < raizInteiraDe + 1,
                           ou seja, 0 <= raizInteiraDe² <= x < (raizInteiraDe + 1)².*/
int raizInteiraDe(int const x)
{
    int r = 0;

    // CI: 0 <= r² e r² <= x.
    while((r + 1) * (r + 1) <= x)
        ++r;
    return r;
}