Resolução da 7ª Aula Prática

Resoluções

1.  Ver ex1.C.  

Atenção!  Os nomes i e j para ciclos usam-se 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:
       
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:
     
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:
     
É 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.

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:
       
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:
     
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:
     
É 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.

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 aluno.