Guião da 7ª Aula Prática

Os dois primeiros exercícios devem ser feitos por alunos no quadro, em conversa com colegas e docente.  O exercício 3.a) deve ser feito pelos alunos.  Quando faltarem 30 min para o final da aula, o docente deve chamar alguém ao quadro e terminar a demonstração no tempo disponível.  Deve ficar muito clara a demonstração (poucas rasuras, etc.).

Resoluções

1.  Ver ex1.C.  

Atenção!  Neste exercício é conveniente dizer que os nomes i e j para ciclos se usam apenas por tradição.  Melhor seria, neste caso, usar numero_de_naturais_ja_somados.

Demonstração de correcção:

  1. Escrever claramente a pré-condição (PC) e a condição objectivo (CO).  Este passo corresponde à especificação do problema:
      2.        
      PC      : 0 <= n.
      CO: r = (S j : 0 <= j < n : j + 1).
      sendo esta a condição objectivo antes do retorno!
          
  2. Determinar a condição invariante CI que permite provar que CI e ¬G implica CO:
      3.      
      CI      : r = (S j : 0 <= j < i : j + 1) e 0 <= i <= n.

      CI e ¬G é r = (S j : 0 <= j < i : j + 1) e 0 <= i <= n e i = n, que claramente implica CO.
            

  3. Verificar que é de facto uma condição invariante: que é verdadeira após a inicialização, e que o facto de CI e G serem verdadeiras antes do passo leva forçosamente a ser verdadeira depois do passo CI:
      4.      
      É evidente que a condição invariante é verdadeira depois da inicialização, pois um somatório com zero termos tem valor nulo.

      O passo do ciclo consiste na acção e no progresso seguintes:
       

        // Aqui sabe-se que CI e G: r = (S j : 0 <= j < i : j + 1) e 0 <= i <= n e i <> n,
        // ou seja, r = (S j : 0 <= j < i : j + 1) e 0 <= i < n.
        r += i + 1;
        ++i;
        // Pretende-se demonstrar que aqui CI é verdadeira, ou seja,
        // r = (S j : 0 <= j < i : j + 1) e 0 <= i <= n.

      A demonstração parte dos objectivos.  Qual a condição mais fraca a impor antes do progresso para que CI seja verdadeira depois?  Substituindo i por i + 1, fica
       

        // r = (S j : 0 <= j < i + 1 : j + 1) e 0 <= i + 1 <= n, ou seja,
        // r = (S j : 0 <= j < i + 1 : j + 1) e -1 <= i <= n - 1, ou seja,
        // r = (S j : 0 <= j < i + 1 : j + 1) e -1 <= i < n.
        ++i;
        // r = (S j : 0 <= j < i : j + 1) e 0 <= i <= n.

      Qual a condição mais fraca a impor antes da acção?  Substituindo r por r + i + 1, fica
       

        // r + i + 1 = (S j : 0 <= j < i + 1 : j + 1) e -1 <= i < n.
        r += i + 1; // equivalente a r = r + i + 1;
        // r = (S j : 0 <= j < i + 1 : j + 1)  e -1 <= i < n.

      A demonstração completa-se verificando que, de facto,
       

        r = (S j : 0 <= j < i : j + 1) e 0 <= i < n
        implica
        r + i + 1 = (S j : 0 <= j < i +1 : j + 1) e -1 <= i < n.
               
  4. Provar que o ciclo termina.

      5. Como, pela PC, 0 <= n e i começa com 0 e é incrementado de 1 a cada passo do ciclo, o ciclo termina sempre ao fim de n iterações.

2.a)  Ver ex2a.C.  Demonstração de correcção:

  1. Abaixo escreve-se m por multiplicador e M por multiplicando.
         
  2. Escrever claramente a pré-condição (PC) e a condição objectivo (CO).  Este passo corresponde à especificação do problema:
      3.        
      PC      : 0 <= m.
      CO: r = m × M.
      sendo esta a condição objectivo antes do retorno!
          
  3. Determinar a condição invariante CI que permite provar que CI e ¬G implica CO:
      4.      
      CI      : r = i × M e 0 <= i <= m.

      CI e ¬G é r = i × M e 0 <= i <= m e i = m, que claramente implica CO.
            

  4. Verificar que é de facto uma condição invariante: que é verdadeira após a inicialização, e que o facto de CI e G serem verdadeiras antes do passo leva forçosamente a ser verdadeira depois do passo CI:
      5.      
      É evidente que a condição invariante é verdadeira depois da inicialização.

      O passo do ciclo consiste na acção e no progresso seguintes:
       

        // Aqui sabe-se que CI e G: r = i × M e 0 <= i <= m e i <> m, ou seja,
        // r = i × M e 0 <= i < m.
        r += M;
        ++i;
        // Pretende-se demonstrar que aqui CI é verdadeira, ou seja,
        // r = i × M e 0 <= i <= m.

      A demonstração parte dos objectivos.  Qual a condição mais fraca a impor antes do progresso para que CI seja verdadeira depois?  Substituindo i por i + 1, fica
       

        // r = (i + 1) × M e 0 <= i + 1 <= m, ou seja,
        // r = i × M + M e -1 <= i <= m - 1, ou seja,
        // r = i × M + M e -1 <= i < m.
        ++i;
        // r = i × M e 0 <= i <= m.

      Qual a condição mais fraca a impor antes da acção?  Substituindo r por r + i + 1, fica
       

        // r + M = i × M + M  e -1 <= i < m.
        r += M; // equivalente a r = r + M;
        // r = i × M + M  e -1 <= i < m.

      A demonstração completa-se verificando que, de facto,
       

        r = i × M e 0 <= i < m.
        implica
        r + M = i × M + M  e -1 <= i < m.
               
  5. Provar que o ciclo termina.

      6.  Como, pela PC, 0 <= m e i começa com 0 e é incrementado de 1 a cada passo do ciclo, o ciclo termina sempre ao fim de m iterações.

2.b)  Ver ex2b.C.  É conveniente começar por arbitrar a multiplicação por dois como progresso e, depois, vez qual a acção que permite recuperar a condição invariante.  Depois concluir que isso só acontece se se souber adicionalmente que 2 × i <= m.  Porquê multiplicar por dois, e não incrementar?  Porque se obtém uma progressão geométrica, e não aritmética, o que leva o ciclo a terminar mais cedo.  Notar que:

  1. O progresso rápido só pode ser usado quando 2 × i <= m, pois de outra forma ultrapassava-se o valor que permite ao ciclo terminar.
  2. O progresso rápido não pode ser usado quando i = 0, pois não haveria qualquer progresso real!  O ciclo não terminaria.

A demonstração de correcção é simples, e fica como exercício para o... docente :-).

3.a)  Ver ex3a.C.  Demonstração de correcção:

  1. Escrever claramente a pré-condição (PC) e a condição objectivo (CO).  Este passo corresponde à especificação do problema:
      2.        
      PC      : 0 <= n.
      CO: r = (S j : 0 <= j < n : 2 × j + 1).
      sendo esta a condição objectivo antes do retorno!
          
  2. Determinar a condição invariante CI que permite provar que CI e ¬G implica CO:
      3.      
      CI      : r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i <= n.

      CI e ¬G é r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i <= n e i = n, que claramente implica CO.
            

  3. Verificar que é de facto uma condição invariante: que é verdadeira após a inicialização, e que o facto de CI e G serem verdadeiras antes do passo leva forçosamente a ser verdadeira depois do passo CI:
      4.      
      É evidente que a condição invariante é verdadeira depois da inicialização, pois um somatório com zero termos tem valor nulo.

      O passo do ciclo consiste na acção e no progresso seguintes:
       

        // Aqui sabe-se que CI e G: r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i <= n e i <> n,
        // ou seja, r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i < n.
        r += 2 * i + 1;
        ++i;
        // Pretende-se demonstrar que aqui CI é verdadeira, ou seja,
        // r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i <= n.

      A demonstração parte dos objectivos.  Qual a condição mais fraca a impor antes do progresso para que CI seja verdadeira depois?  Substituindo i por i + 1, fica
       

        // r = (S j : 0 <= j < i + 1 : 2 × j + 1) e 0 <= i + 1 <= n, ou seja,
        // r = (S j : 0 <= j < i + 1 : 2 × j + 1) e -1 <= i <= n - 1, ou seja,
        // r = (S j : 0 <= j < i + 1 : 2 × j + 1) e -1 <= i < n.
        ++i;
        // r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i <= n.

      Qual a condição mais fraca a impor antes da acção?  Substituindo r por r + i + 1, fica
       

        // r + 2 × i + 1 = (S j : 0 <= j < i + 1 : 2 × j + 1) e -1 <= i < n.
        r += 2 * i + 1; // equivalente a r = r + 2 * i + 1;
        // r = (S j : 0 <= j < i + 1 : 2 × j + 1)  e -1 <= i < n.

      A demonstração completa-se verificando que, de facto,
       

        r = (S j : 0 <= j < i : 2 × j + 1) e 0 <= i < n
        implica
        r + 2 × i + 1 = (S j : 0 <= j < i +1 : 2 × j + 1) e -1 <= i < n.
               
  4. Provar que o ciclo termina.

      5.  Como, pela PC, 0 <= n e i começa com 0 e é incrementado de 1 a cada passo do ciclo, o ciclo termina sempre ao fim de n iterações.

3.b)  Conclui-se que antes de desenvolver um ciclo é necessário perceber se não haverá formas mais simples de resolver o problema...  Conclui-se que a matemática é útil, se é que ainda era necessário.

4.a) a 4.c)  Ver ex4abc.C.

4.d)  

(Abaixo escreve-se m por limite_inferior, n por limite_superior e s por passo.)

No último ciclo não se pode usar a guarda i != n.  A razão é simples: nem todos os possíveis valores de m e de s são tais que i acabe por tomar exactamente o valor n.  E, se isso não acontecer, o ciclo é infinito...  É interessante escrever a condição objectivo e a condição invariante do ciclo da alínea 4.c)

CO:  Foram escritos todos os inteiros entre m e n exclusive de s em s.

e

CI:  Foram escritos já todos os inteiros entre m e i exclusive de s em s, sendo que i = m + k × s, para algum k, e que m <= i < n + s.

A grande diferença face à condição invariante do primeiro ciclo, alínea 4.a), é, para além do passo (que se reflecte nos possíveis valores de i), o limite superior de i.  É que escrever como limite superior i <= n torna impossível determinar uma guarda tal que CI e ¬G implica CO.  Porquê?  Porque as guardas possíveis são G: i <> n ou G: i < n (cujas negações são ¬G: i = n ou ¬G: i >= n), que conduzem a uma condição que pode ser impossível de satisfazer: i = n e i = m + k × s para algum k.  Daí a necessidade de enfraquecer ainda mais a condição invariante do que o usual, escrevendo como limite superior para a variação de i que i < n + s.  Neste caso a guarda a escolher é G: i < n, pois leva a que, no final do ciclo, se tenha:

i = m + k × s para algum k e m <= i < n + s e n <= i,

ou seja

i = m + k × s para algum k e n <= i < n + s,

que é o mesmo que

i = m + k × s para algum k e n <= i e i - s < n,

ou seja,

i = m + k × s para algum k e i - s < n e n <= i,

pelo que se conclui que

CI e ¬G:  Foram escritos já todos os inteiros entre m e i exclusive de s em s, sendo que i = m + k × s para algum k e que i - s < n e n <= i.

Note-se que o último inteiro escrito (se é que algum inteiro foi escrito) é exactamente i - s, que é inferior a n como pretendido, e que o inteiro seguinte seria já i, que pelo último termo da asserção acima está já fora do intervalo pretendido.  Logo, CI e ¬G implica CO como se pretendia.