Aula 9

Resolução dos exercícios

Exercício 1.a)

Esta função recorre a um ciclo. A PC e a CO do ciclo podem facilmente ser expressas como se segue:

PC: n >= 0, m = m
CO: (Q k : 0 <= k < n : m[k] = m[n - 1 - k])

Qual a condição invariante? Usando a técnica usual de substituir uma das constantes no quantificador por uma nova variável de programa, obtem-se:

CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e 0 <= i <= n

Donde a guarda surge naturalmente como G: i != n, e uma possível inicialização é:

i = 0;

pois conduz trivialmente à veracidade da CI. Um possível progresso é simplesmente

i++;

pois conduz necessariamente à terminação do ciclo. Mas que acção utilizar? No passo do ciclo tem-se CI e G, ou seja

(Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e 0 <= i <= n e i <> n

o que implica

(Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e 0 <= i + 1 <= n

Para que a CI seja recuperada, apesar do progresso, é necessário que a acção conduza a

(Q k : 0 <= k < i + 1 : m[k] = m[n - 1 - k]) e 0 <= i + 1 <= n

ou seja

(Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e m[i] = m[n - 1 - i] e 0 <= i + 1 <= n

Mas a atribuição

m[i] = m[n - 1 - i];

não é possível, pois m é uma variável matemática usada para representar os valores originais na matriz m! A atribuição

m[i] = m[n - 1 - i];

já é possível, mas, como não se garante que m[n - 1 - i] = m[n - 1 - i], não conduz necessariamente, em conjunto com o progresso, à CI.

A conclusão que se pode tirar do falhanço anterior é que a CI tem de afirmar não só que os primeiros i elementos de m estão já trocados, como tem de afirmar alguma coisa acerca dos restantes elementos da matriz. Em particular, seria desejável (aparentemente) que, para que a atribuição m[n - 1 - i] = m[n - 1 - i] surtisse o efeito desejado, os restantes elementos estivessem pela ordem original. Assim, uma nova versão da CI é

CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : i <= k < n : m[k] = m[k]) e
0 <= i <= n

Mas esta solução só resolve o problema quando i <= n - 1 - i, pois só nessas circunstâncias a CI garante que m[n - 1 - i] = m[n - 1 - i]. Ou seja, só se consegue recuperar o invariante para 2 i <= n - 1, i.e., para metade da matriz! Isto acontece porque os valores originalmente à esquerda da matriz se perderam no processo de troca! I.e., o ciclo

i = 0;
while(i != n) {
m[i] = m[n - 1 - i];
i++;
}

quando aplicado a uma matriz, só consegue inverter a primeira metade da matriz. Por exemplo, se n = 6 e m contiver originalmente

quando i atingir 3 conterá

Isto demonstra que a CI desenvolvida não é apropriada! Como melhorá-la? Aparentemente seria necessário que, quando i atingisse sensivelmente metade dos elementos da matriz, esta já estivesse totalmente ordenada. Mas para isso a CI tem de obrigar não apenas os i primeiros elementos a estarem invertidos, mas também os i últimos! Ajustando a CI:

CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i <= n

Ou seja, a nova CI divide a matriz em três partes:

Esquerda, já invertida, para índices entre 0 e i - 1.
Central, por inverter, para índices entre i e n - 1 - i.
Direita, já invertida, para índices entre n - i e n - 1.

Falta agora verificar de novo qual a guarda mais apropriada a utilizar. Para que CI e ~ G => CO, é necessário escolher uma guarda cuja negação reduza a gama de valores da terceira conjunção da CI a zero, ou seja, conduza a que todos os valores estejam invertidos. Para isso tem de se fazer i = n - i, ou seja, 2 i = n. Mas esta equação só tem solução para n par! Que acontece para n ímpar? Observe-se um exemplo

Depois de invertida, a matriz passará a conter

Ou seja, o elemento central pode manter-se na sua posição. Assim, quando n for ímpar, a negação da guarda deverá conduzir a que o quantificador da terceira conjunção contenha um único elemento, o que se consegue obrigando a que i = n - 1 - i, ou 2 i + 1 = n.

Resumindo, se n for par, a negação da guarda deverá ser 2 i = n, e se n for ímpar, a negação da guarda deverá ser 2 i + 1 = n. Mas estas são as equações da divisão inteira de n por 2, sendo i o quociente! Assim, a negação da guarda pode ser escrita simplesmente como i = n // 2, ou seja G: i <> n // 2.

Mas, nesse caso, a CI pode ser um pouco mais forte, pois a gama de valores admitida para i é ainda demasiado grande. Pode-se estringir esta gama para 0 <= i <= n // 2, ou seja

CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i <= n // 2

Esta alteração da CI revelar-se-á muito útil para a determinação da acção do ciclo.

Em resumo, a CI e a G são:

CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i <= n // 2
G: i <> n // 2

A inicialização do ciclo faz-se, mais uma vez, fazendo simplesmente

i = 0;

pois conduz imediatamente à veracidade da CI. Quanto ao progresso, também é fácil verificar que a simples incrementação de i conduz forçosamente à terminação do ciclo, ou seja, o progresso é

i++;

Para determinar qual a acção do ciclo, começa-se, como habitual, por observar que, no passo do ciclo, CI e G é verdadeira, ou seja

(Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i <= n // 2 e i <> n // 2

donde se tira facilmente que

(Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i + 1 <= n // 2

Ora, como i < n // 2, então necessariamente 2 i < n, ou seja, 2 i <= n - 1, ou ainda i <= n - i - 1. Mas isso significa que, pela terceira conjunção da CI acima, m[i] = m[i] e m[n - i - 1] = m[n - i - 1].

O objectivo da acção é recuperar a CI apesar do progresso. Ou seja, desejar-se-ia que, antes do progresso,

(Q k : 0 <= k < i + 1: m[k] = m[n - 1 - k]) e (Q k : n - i - 1 <= k < n : m[k] = m[n - 1 - k]) e
(Q k : i + 1 <= k < n - i - 1 : m[k] = m[k]) e 0 <= i + 1 <= n // 2

A quarta conjunção ficou já demonstrado que se verifica mesmo antes da acção. Quanto à terceira conjunção, um vez que o quantificador apenas perde termos no processo, verifica-se também mesmo sem a acção. Quanto às duas primeira conjunções,

(Q k : 0 <= k < i + 1: m[k] = m[n - 1 - k]) = (Q k : 0 <= k < i: m[k] = m[n - 1 - k]) e
m[i] = m[n - 1 - i]
(Q k : n - i - 1 <= k < n : m[k] = m[n - 1 - k]) = (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
m[n - i - 1] = m[i]

Mas, como se viu acima, m[i] = m[i] e m[n - i - 1] = m[n - i - 1], pelo que a acção deverá simplesmente trocar os valores de m[i] e m[n - i - 1]. Por exemplo:

int aux = m[i];
m[i] = m[n - i - 1];
m[n - i - 1] = aux;

Ou seja, convertendo para um ciclo for, a função completa é (lembre-se que a // b se escreve simplemente a / b em C++, assumindo que a e b são inteiros)

PC: n >= 0, m = m
CO: (Q k : 0 <= k < n : m[k] = m[n - 1 - k])
void inverte(int m[], int n)
{
    // CI: (Q k : 0 <= k < i : m[k] = m[n - 1 - k]) e
    //       (Q k : n - i <= k < n : m[k] = m[n - 1 - k]) e
    //       (Q k : i <= k < n - i : m[k] = m[k]) e 0 <= i <= n // 2
    for(int i = 0; i != n / 2; i++) {
        aux = m[i];
        m[i] = m[n - i - 1];
        m[n - i - 1] = aux;
    }
}

Exercício 1.b)

// PC: n >= 0
// CO: devolve (Q k : 0 <= k < n - 1 : m[k] <= m[k + 1])
bool éCrescente(int m[], int n)
{
    // n >= 0
    if(n == 0)
        return true;
    // n > 0
    // CI: (é_crescente = (Q k : 0 <= k < i - 1 : m[k] <= m[k + 1])) e 1 <= i <= n
    bool é_crescente = true;
    for(i = 1; é_crescente && i != n; i++)
        é_crescente = m[i - 1] <= m[i];
    return é_crescente;
}

ou, duma forma mais habitual em C++, mas para a qual não há CI evidente (pois não é um ciclo bem comportado, podendo nunca se chegar ao return final)

// PC: n >= 0
// CO: devolve (Q k : 0 <= k < n - 1 : m[k] <= m[k + 1])
bool éCrescente(int m[], int n)
{
    if(n == 0)
        return true;
    for(i = 1; i != n; i++)
        if(m[i - 1] > m[i])
            return false;
    return true;
}

que ainda se costuma ver escrito como

// PC: n >= 0
// CO: devolve (Q k : 0 <= k < n - 1 : m[k] <= m[k + 1])
bool éCrescente(int m[], int n)
{
    for(i = 1; i < n; i++)
        if(m[i - 1] > m[i])
            return false;
    return true;
}

onde se usa uma guarda mais forte para garantir que o ciclo termina quando n= 0 (e também para n = - 1, n = -2, etc.). Esta última versão viola a regra de que as guardas dos ciclos devem ser tão fracas quanto possível.

Exercício 1.c)

A CI obtém-se por factorização da CO.

// PC: n > 0 e (E j : 0 <= j < n : m[j] = k)
// CO: 0 <= i < n e m[i] = k e (Q j : 0 <= j < i : m[j] <> k)
int primeiraOcorrência(int m[], int n, int k)
{
    // CI: 0 <= i < n e (Q j : 0 <= j < i : m[j] <> k)
    int i;
    for(i = 0; m[i] != k; i++)
        continue; // quando a instrução é nula, costuma pôr-se continue
    return i;
}

Note-se que a variável i foi definida fora do ciclo for, pois o seu valor é necessário fora do ciclo for para devolução posterior. Se a variável i fosse definida no próprio ciclo for não seria visível aquando do return (excepto em alguns compiladores mais antigos).

Exercício 1.d)

A parte mais difícil deste exercício é escrever a CO. Em primeiro lugar, seja i a variável devolvida pela função. A primeira observação a realizar é que a gama de valores aceitável para i é 0 <= i <= n. Por outro lado, exista ou não k em m, é evidente que não pode existir nenhum elemento da matriz com índice inferior a i que contenha o valor k. Exprimindo matematicamente: (Q j : 0 <= j < i : m[j] <> k). Finalmente, das duas uma, ou i = n, e portanto k não existe em m, ou i <> n e m[i] = k. Esta última condição pode ser expresa simplesmente como

i = n ou (i <> n e m[i] = k)

que, aplicando a propriedade distributiva da disjunção, é o mesmo que

i = n ou m[i] = k

Assim, a CO é

CO: 0 <= i <= n e (Q j : 0 <= j < i : m[j] <> k) e (i = n ou m[i] = k)

Neste caso a CI do ciclo obtém-se recorrendo, mais uma vez, à factorização da CO:

// PC: n >= 0
// CO: 0 <= i <= n e (Q j : 0 <= j < i : m[j] <> k) e (i = n ou m[i] = k)
int primeiraOcorrência(int m[], int n, int k)
{
    // CI: 0 <= i <= n e (Q j : 0 <= j < i : m[j] <> k)
    int i;
   for(i = 0; i != n && m[i] != k; i++)
        continue; // quando a instrução é nula, costuma pôr-se continue
    return i;
}

O ciclo é muito semelhante ao do exercício anterior, com a diferença de que a G foi reforçada de modo a forçar o ciclo a terminar depois de explorados todos os elementos da matriz (anteriormente não era necessário pois garantia-se que existia um elemento da matriz com o valor procurado).

Exercício 1.e)

Pode-se resolver à custa da função índiceDoMáximo() (ver Índice do maior elemento de uma matriz):

int máximo(int m[], int n)
{
return m[índiceDoMáximo(m, n)];
}