Please enable JavaScript.
Coggle requires JavaScript to display documents.
L11, L12, L13 - Coggle Diagram
L11
Conceito de Refinamento
-
Passagem da representação matemática abstrata (conjuntos, relações) para estruturas de dados mais concretas
-
Operacoes Refinadas
Mantêm nome, parâmetros e saídas da operação abstrata
Comportamento observável preservado, pré-condição pode ser enfraquecida
Provas e Exemplos
Obrigações de prova : inicialização e operações devem refinar a versão abstrata sob o invariante de ligação
Exemplos: Team, Exam, Ironing e Port
-
L13
-
Nao determinismo em B
Construções como ANY, CHOICE, :∈ e
SELECT com várias alternativas
-
Resolucao do Refinamento
Refinar reduz o conjunto de comportamentos permitidos, escolhendo um deles
-
Exemplos do Curso
Allocate, Books, Jukebox e MySet
-