Resumo da Aula 7

Sumário

• Ciclos
  • Estrutura típica de um ciclo
  • Equivalências entre ciclos
  • Exemplo
• Prova de correcção de um ciclo
  • Definições
  • Estrutura de um ciclo com asserções
  • Demonstrar a correcção de um ciclo
    • Demonstração directa
    • Demonstração inversa
• Exemplo de utilização de um ciclo

1  Ciclos

1.1  Estrutura típica de um ciclo

inic
while(G) {
    acção
    prog
}

• inic (inicialização) são instruções que inicializam as variáveis usadas no ciclo;
• G é a guarda do ciclo;
• acção são instruções que apesar do progresso, garantem que o ciclo conduz ao resultado correcto;
• prog (progresso) são instruções que fazem o ciclo progredir em direcção ao seu termo; e
• passo é o nome que se dá à sequência de instruções acção prog.

1.2  Equivalências entre ciclos

Válidas em geral, estas equivalências não são verdadeiras se as instruções controladas incluírem as instruções return, break, continue, ou goto.  Também há diferença quanto ao âmbito de variáveis definidas nestas instruções.

1.3  Exemplo

Exemplo de um ciclo para mostrar no ecrã os inteiros de 0 a 9 (inclusive) construído usando cada uma das três instruções.

while:

int i = 0;
while(i != 10) {
    cout << i << endl;
    ++i;
}
// Neste ponto i é visível.

for(int i = 0; i != 10; ++i)
   cout << i << ' ';
// Neste ponto i não está definida.

int i = 0;
for(; i != 10; ++i)
   cout << i << ' ';
// Neste ponto i é visível.

int i = 0;
do {
    cout << i << ' ';
    ++i;
} while(i != 11);

2  Prova de correcção de um ciclo

inic
while(G) {
    acção
    prog
}

2.1  Definições

• Pré-condição (PC):  É uma condição que se admite ser verdadeira antes da inicialização do ciclo.  Caso não seja verdadeira não se garante que este leve ao objectivo pretendido, i.e., à veracidade da CO.
• Condição objectivo (CO):  É a condição que se pretende que seja verdadeira no final do ciclo e que define qual o seu objectivo.
• Guarda (G):  É a condição de continuação do ciclo.  Enquanto G for verdadeira as instruções acção e prog são executadas.
• Condição invariante (CI):  É uma condição que se mantém verdadeira desde a inicialização (antes de começar a execução da instrução de inicialização) até ao seu fim.  Esta condição também é verdadeira depois do final do ciclo.

2.2  Estrutura de um ciclo com asserções

// PC: admite-se ser verdadeira neste ponto.

inic // inicialização do ciclo.

// CI: deve ser verdadeira neste ponto.

while(G) {
    // CI e G são verdadeiras neste ponto, por construção.

    passo // acção seguida de prog.
    // devem implicar que CI seja verdadeira neste ponto.
}

// CI e ¬G são verdadeiras neste ponto, por construção e
// devem implicar que CO seja verdadeira neste ponto.

2.3  Demonstrar a correcção de um ciclo

1. Provar que, dada a PC, após a inicialização inic a CI é verdadeira;
2. provar que se CI é verdadeira no antes do passo também o é após o passo;
3. provar que CI e ¬G implica CO; e
4. provar que o ciclo termina.

2.4  Demonstração de asserções

É comum haver necessidade de demonstrar que

// PC
instrução
// CO

Ou seja, que, sabendo que a pré-condição PC se verifica, então depois da instrução instrução também se verifica a condição objectivo CO.

Por exemplo:

// PC: 10 <= x.
x = x + 1;
// CO: 0 <= x.

2.4.1  Demonstração directa

A demonstração é feita partindo da pré-condição:

// PC: 10 <= x.
x = x + 1;
// Logo, depois de aumentar x de uma unidade: 11 <= x.

// CO: 0 <= x.

e verificando que a asserção deduzida implica a condição objectivo CO:

// PC: 10 <= x.
x = x + 1;
// 11 <= x implica 
// CO: 0 <= x.

2.4.1  Demonstração inversa

A demonstração é feita partindo da condição objectivo, deduzindo a pré-condição mais fraca da instrução que conduz à veracidade da condição objectivo CO:

// PC: 10 <= x.

// Pré-condição mais fraca: 0 <= x + 1, ou seja, -1 <= x.
x = x + 1;
// CO: 0 <= x.

e verificando que a pré-condição PC implica a pré-condição mais fraca deduzida:

// PC: 10 <= x implica
// -1 <= x.
x = x + 1;
// CO: 0 <= x.

3  Exemplo de utilização de um ciclo

// Programa que "adivinha" a sua idade:
#include <iostream>

using namespace std;

int main()
{
    int maxima = 150;
    int minima = 0;

    while(minima <= maxima) {
        int idade = (minima + maxima) / 2;
        cout << "Você tem " << idade << " anos? ";
        char resposta;
        cin >> resposta;
        if(resposta == 's' or resposta == 'S') {
            cout << "Acertei!" << endl;
            return 0;
        } else {
            cout << "É mais nova(o)? ";
            cin >> resposta;
            if(resposta == 's' or resposta == 'S')
                maxima = idade - 1;
            else
                minima = idade + 1;
        }
    }
    cout << "Você enganou-me! Alguma idade há-de ter..."
         << endl;
}