Resolução da 9ª Aula Prática

Resoluções

1.a) a 1.d) Ver ex1abcd.C.

2.a) Ver ex2a.C.

Seja dim(m) a dimensão da matriz passada como argumento. O esqueleto da função é:

/** Devolve o índice da primeira ocorrência de v em m.
    @pre (E j : 0 <= j < dim(m) : m[j] = v).
    @post 0 <= indiceDe < dim(m) e m[indiceDe] = v e (Q j : 0 <= j < indiceDe : m[j] <> v). */
int indiceDe(int const m[], int const v)
{
    int indice_de = ?;

    ...

    // CO: 0 <= indice_de < dim(m) e m[indice_de] = v e (Q j : 0 <= j < indice_de : m[j] <> v).
    return indice_de;
}

Como a condição objectivo é uma conjunção, pode-se tentar usar a factorização para obter a condição invariante. Por exemplo,

CI: 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de : m[j] <> v).
G: m[indice_de] <> v.

Qual a inicialização a usar? A mais simples é a inicialização de indice_de com zero

int indice_de = 0;

pois dessa forma a condição invariante fica

CI: 0 <= 0 < dim(m) e (Q j : 0 <= j < 0 : m[j] <> v).

que é verdadeira porque, sendo a pré-condição verdadeira, então de certeza que 0 < dim(m), e porque a conjunção de zero termos é verdadeira.

Qual o progresso a utilizar? A forma mais simples de progredir é incrementar o índice, pelo que o passo fica:

// Aqui sabe-se que:
// CI e G: 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de : m[j] <> v) e m[indice_de] <> v, ou seja,
// 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de + 1 : m[j] <> v).
acção
++indice_de;
// Aqui pretende-se que:
// CI: 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de : m[j] <> v).

Primeiro começa-se por observar que, se é verdade que (Q j : 0 <= j < indice_de + 1 : m[j] <> v), ou seja, que todos os elementos da matriz entre 0 e indice_de inclusive são diferentes de v, então indice_de < dim(m) - 1, pois de outra forma o valor v não existiria na matriz, o que é contraditório com a pré-condição da função. Logo,

// Aqui sabe-se que:
// 0 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v).
acção
++indice_de;
// Aqui pretende-se que:
// CI: 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de : m[j] <> v).

Verifique-se qual a pré-condição mais fraca para que, depois do progresso, se verifique a condição invariante:

// 0 <= indice_de + 1 < dim(m) e (Q j : 0 <= j < indice_de + 1 : m[j] <> v), ou seja,
// -1 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v).
++indice_de;
// CI: 0 <= indice_de < dim(m) e (Q j : 0 <= j < indice_de : m[j] <> v).

Logo, a acção tem de ser tal que:

// 0 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v).
acção
// implica -1 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v).

Mas então conclui-se que não é necessária qualquer acção, visto que

0 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v)
implica -1 <= indice_de < dim(m) - 1 e (Q j : 0 <= j < indice_de + 1 : m[j] <> v)

A função completa fica simplesmente:

/** Devolve o índice da primeira ocorrência de v em m.
    @pre (E j : 0 <= j < dim(m) : m[j] = v).
    @post 0 <= indiceDe < dim(m) e m[indiceDe] = v e (Q j : 0 <= j < indiceDe : m[j] <> v). */
int indiceDe(int const m[], int const v)
{
    assert(?);

    int indice_de = 0;

    while(m[indice_de] != v)
        ++indice_de;

    assert(m[indice_de] = v);

    return indice_de;
}

A demonstração de correcção total do ciclo implica verificar que termina ao fim de um número finito de passos. Seja k um valor entre 0 e dim(m) exclusive tal que m[k] = v. Que esse valor existe é óbvio pela pré-condição da função. Mas então o ciclo termina desde que indice_de, que começa em zero, atinja o valor k, o que acontece garantidamente ao fim de k passos, ou seja, na pior das hipóteses ao fim de n - 1 passos (se o valor que se procura constar apenas na última posição da matriz).

Como verificar as pré-condições? Explicar que para se invocar outra função, a dimensão tem de ser recebida como parâmetro.

2.b) Ver ex2b.C.

2.c) Ver ex2c.C.

Esqueleto:

/** Devolve o índice da primeira ocorrência de valor em v ou o número de itens do
    vector se o valor não existir.
    @pre V.
    @post ?. */
vector<int>::size_type indiceOuTamanhoDe(vector<int> const v, int const valor)
{
    vector<int>::size_type i = ?;
   ...
    // CO: ?.    return i;
}

A CO pode ser escrita como:

CO: (0 <= i < v.size() e v[i] = valor e (Q j : 0 <= j < i : v[j] <> valor)) ou
((Q j : 0 <= j < v.size() : v[j] <> valor) e i = v.size()).

que pode ser escrita como

CO: (0 <= i < v.size() e v[i] = valor e (Q j : 0 <= j < i : v[j] <> valor)) ou
((Q j : 0 <= j < i : v[j] <> valor) e i = v.size()).

ou ainda, acrescentando um conjunção inocente ao segundo termo do ou

CO: (0 <= i < v.size() e v[i] = valor e (Q j : 0 <= j < i : v[j] <> valor)) ou
((Q j : 0 <= j < i : v[j] <> valor) e 0 <= i <= v.size() ei = v.size()).

e fazendo uma pequena manipulação ao primeiro termo

CO: (0 <= i <= v.size() e i <> v.size() e v[i] = valor e (Q j : 0 <= j < i : v[j] <> valor)) ou
((Q j : 0 <= j < i : v[j] <> valor) e 0 <= i <= v.size() e i = v.size()).

podemos agora pôr em evidência dois termos:

CO: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e
((i <> v.size() e v[i] = valor) ou i = v.size()).

o segundo termo pode ser escrito como

CO: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e (v[i] = valor ou i = v.size()).

Aqui há que explicar que o primeiro termo só tem sentido se o segundo for falso, pelo que se inverte a ordem dos termos (o famoso e não ensinado ou-condicional):

CO: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e (i = v.size() ou v[i] = valor).

Moral da história? A forma como se escreve a CO tem implicações no desenvolvimento. O melhor é começar pela CO mais simples. E que é perfeitamente compreensível!

Esta condição objectivo pode ser factorizada de forma elementar:

CI: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor).
¬G: i = v.size() ou v[i] = valor, ou seja,
G: i <> v.size() e v[i] <> valor.

A inicialização é simplesmente

vector<int>::size_type i = 0;

pois a condição invariante fica

CI: 0 <= 0 <= v.size() e (Q j : 0 <= j < 0 : v[j] <> valor), ou seja,
CI: V e V = V.

O progresso? Simples incrementação. O ciclo termina de certeza, pois i atingirá fatalmente v.size(). Logo, determinando a pré-condição mais fraca do progresso do passo:

// CI e G: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e i <> v.size() e
// v[i] <> valor, ou seja,
// CI e G: 0 <= i < v.size() e (Q j : 0 <= j < i : v[j] <> valor) e v[i] <> valor.
acção
// 0 <= i + 1 <= v.size() e (Q j : 0 <= j < i + 1 : v[j] <> valor), ou seja,//-1 <= i < v.size() e (Q j : 0 <= j < i + 1 : v[j] <> valor).++i; //CI: 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor).

Conclui-se que não é necessário nenhuma acção:

/** Devolve o índice da primeira ocorrência de valor em v ou o número de itens do
    vector se o valor não existir.
    @pre V .
    @post 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e
          (i = v.size() ou v[i] = valor). */
vector<int>::size_type indiceOuTamanhoDe(vector<int> const v, int const valor)
{
    vector<int>::size_type i = 0;
    while(i != v.size() and v[i] != valor)         ++i;
    assert(i == v.size() or v[i] == valor);
    return i;
}

Pode-se simplificar o ciclo se se acrescentar o valor a procurar no final, de forma a servir de sentinela:

/** Devolve o índice da primeira ocorrência de valor em v ou o número de itens do
    vector se o valor não existir.
    @pre v = v.
    @post 0 <= i <= v.size() e (Q j : 0 <= j < i : v[j] <> valor) e
          (i = v.size() ou v[i] = valor) e v = v. */
vector<int>::size_type indiceOuTamanhoDe(vector<int> v, int const valor)
{
    vector<int>::size_type i = 0;
    v.push_back(valor);
    while(v[i] != valor)         ++i;
    v.pop_back();
    assert(i == v.size() or v[i] == valor);
    return i;
}

Pode-se eliminar a instrução v.pop_back();, pois o vector é uma cópia local à função. Nesse caso é conveniente ajustar a instrução de asserção final.