Guiã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).

Discutir com eles 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;
}

Pedir aos alunos a CO.  Provavelmente chegam a:

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() e i = 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.

3.  Ver ex3.C.

4.  Ver ex4.C.

5.  Ver ex5.C.

Começa por se escrever o esqueleto da função, determinando-se a pré-condição e a condição objectivo:

/** Devolve o máximo valor presente no vector.
    @pre 0 < v.size().
    @post (Q j : 0 <= j < v.size() : v[j] <= maximoDe) e
          (E j : 0 <= j < v.size() : maximoDe = v[j]). */
int maximoDe(vector<int> const& v)
{
    int maximo = ?;

    ...

    // CO: (Q j : 0 <= j < v.size(). : v[j] <= maximo) e
           (E j : 0 <= j < v.size(). : maximo = v[j]).
    return maximo;
}

Para obter a condição invariante e a guarda pode-se substituir o limite superior dos quantificadores por uma variável introduzida para o efeito:

CI: (Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
      0 <= i <= v.size().

¬G:  i = v.size(), ou seja,
G:  i <> v.size().

A inicialização é simples, bem como o progresso:

/** Devolve o máximo valor presente no vector.
    @pre 0 < v.size().
    @post (Q j : 0 <= j < v.size() : v[j] <= maximoDe) e
          (E j : 0 <= j < v.size() : maximoDe = v[j]). */
int maximoDe(vector<int> const& v)
{
    int maximo = v[0];
    vector<int>::size_type i = 1;

    while(i != v.size()) {
        acção
        ++i;
    }

    // CO: (Q j : 0 <= j < v.size(). : v[j] <= maximo) e
           (E j : 0 <= j < v.size(). : maximo = v[j]).
    return maximo;
}

Para a determinação da acção, mais uma vez se obtém a pré-condição mais fraca do progresso:

// CI: (Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
//    0 <= i <= v.size().
acção
// (Q j : 0 <= j < i + 1 : v[j] <= maximo) e (E j : 0 <= j < i + 1 : maximo = v[j]) e
// -1 <= i < v.size().
++i;
// CI: (Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
//    0 <= i <= v.size().

A acção não alterará i.  Mas também não há nenhuma atribuição simples que resolva o problema.  Há que distinguir casos.

Hipótese 1: v[i] <= maximo

Nesse caso,

// (Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
// 0 <= i <= v.size() e v[i] <= maximo.
acção
// (Q j : 0 <= j < i + 1 : v[j] <= maximo) e (E j : 0 <= j < i + 1 : maximo = v[j]) e
// -1 <= i < v.size().

é evidente que não é necessária nenhuma acção.  O valor de maximo está correcto.

Hipótese 2: maximo < v[i]

Nesse caso,

// (Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
// 0 <= i <= v.size() e maximo < v[i].
acção
// (Q j : 0 <= j < i + 1 : v[j] <= maximo) e (E j : 0 <= j < i + 1 : maximo = v[j]) e
// -1 <= i < v.size().

é evidente que o valor de maximo tem de ser actualizado, passando a ser v[i].  Ou seja, a acção deverá ser:

maximo = v[i];

Obtendo a pré-condição mais fraca,

// (Q j : 0 <= j < i + 1 : v[j] <= v[i]) e (E j : 0 <= j < i + 1 : v[i] = v[j]) e
// -1 <= i < v.size().
maximo = v[i];
// (Q j : 0 <= j < i + 1 : v[j] <= maximo) e (E j : 0 <= j < i + 1 : maximo = v[j]) e
// -1 <= i < v.size(), ou seja,
// (Q j : 0 <= j < i + 1 : v[j] <= v[i]) e V e -1 <= i < v.size(), ou seja,
// (Q j : 0 <= j < i + 1 : v[j] <= v[i]) e -1 <= i < v.size().

Para confirmar a escolha da acção, basta verificar a implicação

(Q j : 0 <= j < i : v[j] <= maximo) e (E j : 0 <= j < i : maximo = v[j]) e
0 <= i <= v.size() e maximo < v[i].
implica
(Q j : 0 <= j < i + 1 : v[j] <= v[i]) e -1 <= i < v.size().

Por partes:

a)

(Q j : 0 <= j < i : v[j] <= maximo) e maximo < v[i].
implica
(Q j : 0 <= j < i : v[j] <= v[i]).
implica
(Q j : 0 <= j < i + 1 : v[j] <= v[i]), pois o termo acrescentado é v[i] = v[i].

b)

0 <= i <= v.size().
implica
-1 <= i < v.size().

Logo, a função fica:

/** Devolve o máximo valor presente no vector.
    @pre 0 < v.size().
    @post (Q j : 0 <= j < v.size() : v[j] <= maximoDe) e
          (E j : 0 <= j < v.size() : maximoDe = v[j]). */
int maximoDe(vector<int> const& v)
{
    assert(0 < v.size());

    int maximo = v[0];
    vector<int>::size_type i = 1;

    while(i != v.size()) {
        if(maximo < v[i])
            maximo = v[i];
        ++i;
    }

    return maximo;
}

6.  Ver ex6.C.

Começa por se escrever o esqueleto da função, determinando-se a pré-condição e a condição objectivo:

/** Indica se os itens do vector estão por ordem não-decrescente.
    @pre V.
    @post eCrescente = (Q j : 0 <= j < v.size() - 1: v[j] <= v[j + 1]). */
bool eCrescente(vector<int> const& v)
{
    if(v.size() < 2U)
        return true;

    // PC: 2 <= v.size().

    bool e_crescente = ?;

    ...

    // CO: e_crescente = (Q j : 0 <= j < v.size() - 1 : v[j] <= v[j + 1]).
    return e_crescente;
}

Aproveitou-se para resolver os casos patológicos com uma instrução condicional.

Para obter a condição invariante e a guarda pode-se substituir o limite superior do quantificador por uma variável introduzida para o efeito:

CI: e_crescente = (Q j : 0 <= j < i : v[j] <= v[j + 1]) e 0 <= i <= v.size() - 1.

¬G:  i = v.size() - 1, ou seja,
G:  i <> v.size() - 1.

A inicialização é simples, bem como o progresso:

/** Indica se os itens do vector estão por ordem não-decrescente.
    @pre V.
    @post eCrescente = (Q j : 0 <= j < v.size() - 1 : v[j] <= v[j + 1]). */
bool eCrescente(vector<int> const& v)
{
    if(v.size() < 2U)
        return true;

    // PC: 2 <= v.size().

    bool e_crescente = true;
    vector<int>::size_type i = 0;

    while(i != v.size() - 1) {
        acção
        ++i;
    }

    // CO: e_crescente = (Q j : 0 <= j < v.size() - 1 : v[j] <= v[j + 1]).
    return e_crescente;
}

Para a determinação da acção, mais uma vez se obtém a pré-condição mais fraca do progresso:

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

A acção terá de ser escolhida de modo a que

// CI e G: e_crescente = (Q j : 0 <= j < i : v[j] <= v[j + 1]) e 0 <= i < v.size() - 1.
acção
// e_crescente = (Q j : 0 <= j < i + 1 : v[j] <= v[j + 1]) e -1 <= i < v.size() - 1.

É fácil verificar que isso acontece se a acção for:

e_crescente = e_crescente and v[i] <= v[i + 1];

Completando a função, aproveitando para reforçar a guarda, tal como se fez no caso dos números primos, e transformando num ciclo for,

/** Indica se os itens do vector estão por ordem não-decrescente.
    @pre V.
    @post eCrescente = (Q j : 0 <= j < v.size() - 1 : v[j] <= v[j + 1]). */
bool eCrescente(vector<int> const& v)
{
    if(v.size() < 2U)
        return true;

    bool e_crescente = true;

    for(vector<int>::size_type i = 0; e_crescente and i != v.size() - 1; ++i)
        e_crescente = v[i] <= v[i + 1];

    return e_crescente;
}

7.  Ver ex7.C.

8.  Ver ex8.C.