Programas e Refinamento
Programming from Specifications
Carroll Morgan Prentice-Hall, 1994
[Capítulo 1]
Equipe:
Klaus Cavalcante
Tarcísio Quirino
Raquel 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.
Programas como Contratos:
Refinamento



Se para o cliente, o programa prog2 é melhor
do que o programa prog1, então nós dizemos
prog1
prog2
ou seja, prog2 “refina” prog1.
Visão do cliente
Exemplos:

saída de 220V
resistente a chuva

precisa de 4Mb

saída de 220/110V
resistente a 50m de
profundidade
precisa de 2Mb
Programas Abstratos

Estados inicial e final
estado
inicial

estado
final
Estado




ação
do
programa
variáveis são nomes
valores
mapeamentos de variáveis para valores
Um programa imperativo realiza modificações de
estado
Programas Abstratos

Descrições de estado

Exemplo de estado
Variáveis x, y, e z


x
y
z
2
17
3
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 estado
x = 2  x + z < y  z 4  x = 2 y = 17 z = 3

Um estado satisfaz uma fórmula se aquela fórmula o
descreve
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 é verdade
A declaração F1
F2, significa: em qualquer estado,
F1 é verdade se F2 é verdade
O Operador Equivalência
A declaração F1
F2 verdadeiro
F2, significa: F1 verdadeiro SSE
Programas Abstratos

Especificações: A especificação é a principal
característica dos programas abstratos
w: [ 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 Abstratos
Lei 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 ]
refina
y : [0 x  9 , y ^ 2 = x]
 (1.2) é melhor do que (1.1) pela lei 1.1

(1.2)
(1.1)
Programas Abstratos
Lei 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  ]
refina
y : [0 x  9 , y ^ 2 = x y ]
 (1.3) é melhor do que (1.2) pela lei 1.2

(1.3)
(1.2)
Exercício
1.
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ção
w := E
Lei 1.3 Atribuição
Se pre
pos[w\E], então
w ,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áveis
Definição 1.4 Viabilidade
A especificação w :[pre,pos] é viável se e somente se
pre
(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 default
w :[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 ]

Choice
w :[ true , true ]

skip
Mágica (inexequível)
w :[ true , false ]

choose w
Skip
:[ true , true ]

abort
magic
A maioria destes programas não são escritos
deliberadamente
Programas e Refinamento
Programming from Specifications
Carroll Morgan Prentice-Hall, 1994
[Capítulo 1]
Equipe:
Klaus Cavalcante
Tarcísio Quirino
Raquel Monteiro