Please enable JavaScript.
Coggle requires JavaScript to display documents.
Data Refinement - Coggle Diagram
Data Refinement
L011_L012
Refinement
Estão exatamente no meio do caminho entre máquinas abstratas e implemetanções
Por que REFINEMENTS?
A distância semântica entre a máquina e a implementação pode ser muito grande tornando as obrigações de prova muito grandes, portanto é necessário um meio de campo para simplificar as obrigações de prova
Usuários não sentem as mudanças feitas nessa área
Data refinement
Uma transformação do modelo de dados em algo mais detalhado
Quais dados serão usados e quais operações serão implementadas
Relação por invariant de um dado concreto e um dado abstrato
As variáveis da máquina refinada devem estar relacionadas, via invariant das 2 máquinas, com o comportamento da máquina abstrata
Como a initialisation e as operations funcionam com a nova representação dos dados
Herança de informações estáticas
Todas as partes estáticas da máquina abstrata e das máquinas incluídas
Não possuem acesso para máquinas que a máquinas abstrata SEES ou USES
Não possuem acesso para o valor do estado da máquina abstrata enquanto está sendo executada
Refinements só podem conter
INCLUDES
EXTENDS
PROMOTES
SEES
L012
Refinement of non-determinism
Definir a escolha não deterministica para uma deterministica, para uma 'menos' não deterministica ou uma algoritmica
Exemplos
xx :: NATURAL pode se tornar xx :=0
xx :: NATURAL pode virar
CHOICE xx := 0 OR xx := 1
xx :: NATURAL pode virar
IF yy = 0 THEN xx : (xx /= yy)
ELSIF yy /=0 THEN xx :: 2..7