View
215
Download
0
Category
Preview:
Citation preview
Programas e RefinamentoProgramming from SpecificationsCarroll Morgan Prentice-Hall, 1994
[Capítulo 1]Equipe:Klaus CavalcanteTarcísio QuirinoRaquel Monteiro
Visão Tradicional Programa x Especificação
Programas são executáveis, mas de difícil compreensão.
Especificações são legíveis, de fácil entendimento, mas não são executáveis.
Uma Nova Visão Não há distinção entre especificações e
programas Tudo é programa Nem todos os programas são executáveis
Hierarquia de programação Programas abstratos Programas executáveis (código) Nível intermediário
Projetos Mistura de construtores abstratos e concretos
Programas como Contratos: Refinamento
Cliente Programador Negociação Cliente -> Deseja: programas com maior precisão,
rapidez e aplicabilidade em diferentes contextos. Programador -> Deseja: maior liberdade na
implementação, bem como folga na seleção e apresentação de resultados; deseja ainda, mais informação sobre condições de execução do programa, além do acesso a técnicas de implementação, baratas e padronizadas.
Se para o cliente, o programa prog2 é melhor do que o programa prog1, então nós dizemos prog1 prog2ou seja, prog2 “refina” prog1.
Visão do cliente Exemplos:
saída de 220V saída de 220/110V resistente a chuva resistente a 50m de profundidade precisa de 4Mb precisa de 2Mb
Programas como Contratos: Refinamento
Programas Abstratos Estados inicial e final
Estado variáveis são nomes valores mapeamentos de variáveis para valores
Um programa imperativo realiza modificações de estado
estado final
açãodo
programa
estadoinicial
Programas Abstratos Descrições de estado
Exemplo de estado Variáveis x, y, e z
Nós descrevemos estados ao invés de desenhá-los Dizemos que uma fórmula descreve um estado quando
ela se faz verdadeira pelos mapeamentos do estadox = 2x + z < y z 4x = 2y = 17 z = 3
Um estado satisfaz uma fórmula se aquela fórmula o descreve
xyz
2173
Cálculo de predicados Usamos o cálculo de predicados como linguagem de nossas
formulas. Isto inclui:
Termos ( variáveis, constantes, e funções ) Formulas atômicas ( uma composição entre termos e
operadores relacionais, Ex.: =, <, >=) Formulas proposicionais (uma composição entre
formulas atômicas e conectivos proposicionais, Ex.: , , ¬, , )
Quantificadores ( , ) Quantificadores tipados [ (x:T · A), (x:T · A)]
Cálculo de predicados Os Operadores Vínculo
A declaração F1 F2, significa: em qualquer estado, se F1 é verdade então F2 é verdadeA declaração F1 F2, significa: em qualquer estado, F1 é verdade se F2 é verdade
O Operador Equivalência
A declaração F1 F2, significa: F1 verdadeiro SSE F2 verdadeiro
Programas Abstratos Especificações: A especificação é a principal
característica dos programas abstratosw: [ pre , pos ]
quadro (w): valores que podem ser modificados pré-condição (pre): descreve estados iniciais pós-condição (pos): descreve estados finais Exemplo: faça y a raiz quadrada de x desde
que 0 x 9 y : [0 x 9 , y ^ 2 = x ] (1.1)
Uma especificação captura a intenção sem dar o método
Programas AbstratosLei 1.1 Fortalecimento da pós-condição
Se pos’ pos, então
w :[ pre , pos] w :[ pre , pos’]
Programas Abstratos Refinamento de especificações
Uma especificação é melhorada pelo fortalecimento de sua pós-condição
Exemplo: A especificação
y : [0 x 9 , y ^ 2 = x y ] (1.2) refina
y : [0 x 9 , y ^ 2 = x] (1.1) (1.2) é melhor do que (1.1) pela lei 1.1
Programas AbstratosLei 1.2 Enfraquecimento da pré-
condição
Se pre pre’, então
w :[ pre , pos] w :[ pre’ , pos]
Programas Abstratos Refinamento de especificações:
Uma outra forma de melhoria é conseguida pelo enfraquecimento da pré-condição
Exemplo: A especificação
y : [x 0 , y ^ 2 = x y ] (1.3) refina
y : [0 x 9 , y ^ 2 = x y ] (1.2) (1.3) é melhor do que (1.2) pela lei 1.2
Exercício1. Quais destes refinamentos são válidos? (Use
enfraquecimento da pré-condição e fortalecimento da pós-condição)
Programas Executáveis Código
Linguagem de especificação é muito expressiva Nenhum computador pode executar especificações Construtores executáveis (código)
O Comando de Atribuiçãow := E
Lei 1.3 Atribuição Se pre pos[w\E], entãow ,x:[ pre , pos] w := E
O refinamento total, da especificação para o código; é feito em passos, cada qual introduzindo um pouco mais de executabilidade ou eficiência
Programas ViáveisDefinição 1.4 Viabilidade
A especificação w :[pre,pos] é viável se e somente sepre w:T pos)onde T é o tipo da variável w.
Exemplo: y : [true , y ^ 2 = x y ] (1.4) Isso seria como tentar provar que:true (y:R ·(y ^ 2 = x y
Especificações inviáveis não podem ser implementadas
Algumas abreviações comuns
Abreviação 1.5 Pré-condição defaultw :[pos] é uma abreviação para w :[ true , pos]
Abreviação 1.6 Suposição (Assumption){pre} é uma abreviação para :[ pre , true ]
Programas Executáveis Abreviação
Exemplo: A especificação
{0 x 9} y := sqr(x) (1.5) refina
y : [0 x 9 , y ^ 2 = x y ] (1.2) (1.5) é melhor do que (1.2) pela Abreviação 1.6
Lei 1.7 Especificação simples w := E = w :[w = E]
Algumas abreviações comuns Lei 1.8 Absorção de suposição
{pre’} w :[pre , pos] = w :[ pre’ pre , pos] Assim, uma suposição antes de uma
especificação pode ser absorvida diretamente na pré-condição desta
Programas Extremos Abort
w :[ false , true ] abort Choice
w :[ true , true ] choose w Skip
:[ true , true ] skip Mágica (inexequível)
w :[ true , false ] magic
A maioria destes programas não são escritos deliberadamente
Programas e RefinamentoProgramming from SpecificationsCarroll Morgan Prentice-Hall, 1994
[Capítulo 1]Equipe:Klaus CavalcanteTarcísio QuirinoRaquel Monteiro
Recommended