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