Refinamento de Dados

Estende o refinamento de operações
– O estado da especificação abstrata pode ser
diferente do concreto
– Viabiliza a troca de tipos de dados abstratos por
representações computacionais mais adequadas
– As entradas e saídas têm que permanecer as
mesmas e com os mesmos tipos. Não é possível
o refinamento de interface mas sim dos dados
(são admitido estarem encapsulados)
Refinamento de Dados

Exemplos (informal – ver o PS)
– Controle de pessoas num recinto
– Cálculo da média aritmética e máximo
– Refinamento em etapas
Exemplo de refinamento para
specification statement
 Exemplo de refinamento para
pseudocódigo
 Exemplo de refinamento para pascal

Refinamento Dados – Traduçao para
Specification Statement w:[pre,post]

Esquema de entrada de números da
média (EnterNumber)
– n?,sum,size:[true, sum=sum+n? ^ size = size0 + 1]

Esquema de cálculo da média
– m!:[size <> 0, m! = sum div size]
Refinamento Dados - Pseudocódigo
Procedure ENTER(val n?: IN);
sum := sum + n?;
size := size + 1;
Procedure MEAN(res m!: IR);
m! := sum / size;
Refinamento Dados – Código Pascal
Refinamento de Dados – Exemplo com Etapas

Podemos considerar que:
– State1 é apropriado para uma especificação inicial
– State2 é apropriado para uma etapa de projeto
– State3 é apropriado para uma implementação

Temos que garantir as relações de
correspondência entre cada etapa
(executando as devidas obrigações de prova,
como veremos a seguir)
Refinamento de Dados

Devemos estabelecer uma relação entre o
estado abstrato e o estado concreto
– Isto significa que precisamos determinar como
cada estado abstrato é representado no estado
concreto.
– Definimos então um esquema (normalmente
chamado Retrieve) que captura esta relação
• Suas declarações são equivalentes às do
estado abstrato e concreto
• O predicado que o determina tem que capturar
a relação entre os valores a serem refinados
– Exemplo: diagrama nuvens
Refinamento de Dados

Semelhantemente ao refinamento de
operações precisamos provar os dois
predicados:
– Um sobre a pré condição
– Outro sobre a realização da operação
propriamente dita

A diferença é que agora temos que envolver
o esquema que relaciona os estados abstrato
e concreto.
Refinamento de Dados:
Obrigações de Prova

No caso das pré condições
preAOP Re trieve  preCOP

No caso das operações
preAOP Re trieve  COP  AState' Re trieve' AOP

No caso especial do estado inicial
CInit  AState AInit  Re trieve
Refinamento Funcional de Dados

Quando a relação Retrieve entre dois
estados define uma função total
– Para todo elemento representado no estado
abstrato temos uma representação do mesmo no
estado abstrato (função total entre Astate e
Cstate).

Os exemplos do curso irão tratar apenas
refinamentos de dados funcionais
 Simplifica as obrigações de prova
 Exemplo do diagrama de nuvens
Refinamento Funcional de Dados:
Obrigações de Prova

Temos as mesmas obrigações de prova que
o refinamento comum, entretanto, as
mesmas estão simplificadas como mostrado
a seguir
 Antes de mais nada, para que o Retrieve seja
considerado funcional temos que provar:
CState 1AState Re trieve

Vejamos então os teoremas simplificados
visto que o refinamento já é funcional
Refinamento Funcional de Dados:
Obrigações de Prova

No caso das pré condições (não muda)
preAOP Re trieve  preCOP

No caso das operações (retiramos o
quantificador existencial
preAOP Re trieve  COP  Re trieve'  AOP

No caso especial do estado inicial
CInit  Re trieve  AInit
Refinamento Funcional de Dados

Para o refinamento ser bem sucedido temos
que atravessar o seguinte percurso para toda
opetação disponível na especificação