Verificação de Programas: Prova de Corretude (Hoare)

1. Definição do Comando Iterativo e Condição de Saída (CO)

1. CO: {True} todosaprovados {sim = ∀i=0..n-1 pauta[i].getnota() ≥ 10}

   boolean sim;

2. O comando iterativo é definido como:

   todosaprovados ≡ {inic while(G) {ação progresso}}

3. 2. Invariante de Ciclo (CI) e Variáveis

   CI: CO[n-1 ← k] ∧ -1 ≤ k ≤ n-1

   CI: sim = ∀i=0..k pauta[i].getnota() ≥ 10 ∧ -1 ≤ k ≤ n-1

   int k;

   Nota: k = -1 para facilitar a inicialização.

4. 3. Inicialização (inic)

   inic: {k = -1; sim = true;}

   Justificação: {True} inic {CI}

5. 4. Guarda (G) e Negação da Guarda (¬G)

   ¬G (Condição de Paragem): k == n-1 || !sim

   Justificação: (CI ∧ ¬G) → CO

   G: k != n-1 && sim

6. 5. Progresso

   progresso: k = k + 1;

   Justificação: Para garantir a terminação do ciclo.

7. 6. Ação (ação)

   ação: if (pauta[k+1].getnota() < 10) sim = false;

   Ou, alternativamente: sim = sim && pauta[k+1].getnota() ≥ 10;

   Justificação: {CI ∧ G} {ação progresso} {CI}

Prova Formal da Inicialização (2)

30 de Setembro de 2009

├ {True} inic {CI}

1. {CI[sim ← true]} sim=true; {CI} (ratrib, ratrib)
2. {CI[sim ← true] [k ← -1]} k=-1; {CI[sim ← true]}
3. {CI[sim ← true] [k ← -1]} {k=-1; sim=true;} {CI} (rcs 1, 2)
4. True → CI[sim ← true] [k ← -1] (rt)
5. {True} {k=-1; sim=true;} {CI} (ra 3, 4)

├ (CI ∧ ¬G) → CO

1. (CI ∧ ¬G) → CO (rt)

Prova Formal do Corpo do Ciclo (3)

? ├ {CI ∧ G} {ação progresso} {CI}

1. {CI[k ← k+1]} k=k+1; {CI} (RATRIB)
2. {CI[k ← k+1] [sim ← false]} sim=false; {CI[k ← k+1]} (RATRIB)
3. (CI ∧ G ∧ pauta[k+1].getnota() < 10) → CI[k ← k+1] [sim ← false] (RT)
4. {CI ∧ G ∧ pauta[k+1].getnota() < 10} sim=false; {CI[k ← k+1]} (RA 2, 3)
5. (CI ∧ G ∧ pauta[k+1].getnota() ≥ 10) → CI[k ← k+1] (RT)
6. {CI ∧ G} if (pauta[k+1].getnota() < 10) sim=false; {CI[k ← k+1]} (RCAS 4, 5)
7. {CI ∧ G} {if (pauta[k+1].getnota() < 10) sim=false; k=k+1;} {CI} (RCS 1, 6)

Princípio Geral da Argumentação de Hoare

De facto, a seguinte argumentação é válida para uma Condição Invariante (CI) escolhida:

{CD} inic {CI}, {CI ∧ G} {ação prog} {CI}, ((CI ∧ (¬G)) → CO)

Implica:

{CD} {inic while(G){ação progresso}} {CO}

Como se demonstra recorrendo ao Cálculo de Hoare:

1. 1. {CD} inic {CI} (Hipótese)

2. 2. {CI ∧ G} {ação progresso} {CI} (Hipótese)

3. 3. ((CI ∧ (¬G)) → CO) (Hipótese)

4. 4. {CI} while(G){ação progresso} {CI ∧ (¬G)} (2, RCI)

5. 5. {CI} while(G){ação progresso} {CO} (3, 4, RC)

6. 6. {CD} {inic while(G){ação progresso}} {CO} (1, 5, RCS)