Verificação de Programas: Prova de Corretude (Hoare)
Classificado em Espanhol
Escrito em em
português com um tamanho de 3,72 KB
1. Definição do Comando Iterativo e Condição de Saída (CO)
CO:
{True} todosaprovados {sim = ∀i=0..n-1 pauta[i].getnota() ≥ 10}boolean sim;O comando iterativo é definido como:
todosaprovados ≡ {inic while(G) {ação progresso}}2. Invariante de Ciclo (CI) e Variáveis
CI:
CO[n-1 ← k] ∧ -1 ≤ k ≤ n-1CI:
sim = ∀i=0..k pauta[i].getnota() ≥ 10 ∧ -1 ≤ k ≤ n-1int k;Nota: k = -1 para facilitar a inicialização.
3. Inicialização (inic)
inic: {k = -1; sim = true;}Justificação:
{True} inic {CI}4. Guarda (G) e Negação da Guarda (¬G)
¬G (Condição de Paragem):
k == n-1 || !simJustificação:
(CI ∧ ¬G) → COG:
k != n-1 && sim5. Progresso
progresso: k = k + 1;Justificação: Para garantir a terminação do ciclo.