Exemplo
Especificação:
Dada
uma lista de 3 elementos a saida consiste de um indice que tenha o
valor maximo dessa lista
Maximo (a,b,c)
- Precondição: Entrada tem 3 números a,b,c
- m=a
- retratoAtual: m é o máximo em {a}.
- se (b>m)
m = b
fim do se
- retratoAtual: m é o máximo em {a,b}.
- se (c>m)
m = c
fim do se
- retratoAtual: m é o máximo em {a,b,c}.
- retorna (m)
- Póscondição: retorna o máximo em {a,b,c}.
fim do algoritimo
Estados para elaborar um algoritimo
Pensar em sequencia de
instantâneos em vez de sequencia de ações. Partir da saida para a
entrada pensando de forma a temporal.
Sequencia de instantâneos
- Não perder de vista as variações do estado do
computador
- Uma
vez construida pode se ver todo o caminho claramente
Póscondições e Précondições
- Definir a solução do problema que deve ser resolvido
- Retrato sobre a saida desejada (póscondição)
- Retrato inicial sobre a entrada em particular (précondição)
Começar no meio
- Começar com um retrato estatico sobre o estado que gostaria
que tivesse neste instante
- Esse retrato não precisa dar o valor exato de cada variavel
- Fornecer propriedades gerais e relações entre as diversas
estruturas de dados
- Cada instantâneo torna-se parte de um laço
Preencha com ações
- São instantaneo com o tempo parado
- Ainda não foi considerada nehuma ação
- A etapa final é colocar ações (código) entre os
instantâneos consecutivos
Um passo de cada vez
(passo do bebê)
- Cada um desses blocos de ações pode ser executado de
maneira completamente independente dos outros
- É mais facilconsidrar um de cada vez do que com tudo ao
mesmo tempo
- Pode se completar esses blocos em qq ordem que se
quiser
- Modificar um bloco sem se preocupar com efeito nos outros
Você chegou de viagem
- É assim que deve se preencher o codigo entre os
instantâneos entra o i-ésimo e o (i+1)-ésimo.
- A unica coisa que se sabe é que o i-ésimo
é valido, isso é que garante a independencia dos blocos.
De um passo
- Escrever um codigo simples para executar algumas ações
simples que mudam o estado de modo que o (i+1)-ésimo instante
seja válido.
Demosntração de cada passo
- Pode seer feita de um bloco de cada vez
- Provar que ao para o tempo no i-ésimo instante é
valido e para o tempo no (i+1)-ésimo instante é valido
Demonstração da correção
algoritimo
- Se a entrada incial satisfaza a precondição e o codo
inteiro é executado, então no final, ostado será tal que a póscondição
fica satisfeita. Isso prova que o algoritimo funciona.