Please enable JavaScript.
Coggle requires JavaScript to display documents.
Introdução às máquinas abstratas - Coggle Diagram
Introdução às máquinas abstratas
Bloco de construção mais básico do método B
Descreve o comportamento do sistema, o que o componente pode fazer
Compostas por estados, que indicam as informações que estão armazenadas na máquina abstrata.
As propriedades dessas informações são armazenadas na invariante de estado
Após isso, temos que definirmos a inicialização, ou seja, os valores iniciais dessas variáveis
E, finalmente, determinamos a interface desses componentes
Possui inúmeras seções
Seção Máquina - Damos um nome à máquina.
Seção Variáveis - Listamos as variáveis de estado da máquina.
Seção Invariante - Declaramos as propriedades das variáveis
Seção Inicialização - Damos o comando que inicializa as variáveis de estado
Seção Operações - Listamos as operações que funcionam na máquina
Essas operações são compostas por um nome, parâmetros de entrada e parâmetros de saída
Na declaração da operação podemos restringir as propriedades que devem ser satisfeitas pelos parâmetros e pelo estado atual em que a operação é chamada
Declaramos as mudanças de estado e a geração de saída destas operações
Consistência de máquina
Para ser alcançada devemos garantir que as cláusulas são coerentes e consistentes.
Deve existir valores para as variáveis de estado que satisfaçam o invariante.
Para garantirmos a consistência do isolamento temos que garantir que o estado inicial é consistente com o invariante
Motivos para a inconsistência na máquina
A pré-condição de operação é muito fraca
A pré-condição permite que uma operação seja chamada quando não deveria
A operação está incorreta
A invariante está incorreta