Please enable JavaScript.
Coggle requires JavaScript to display documents.
Máquinas Abstratas e Consistência - Coggle Diagram
Máquinas Abstratas e Consistência
Estrutura da Máquina
MACHINE
Define o nome único do componente do projeto
VARIABLES
Listas as variaveis de estado do sistema
INVARIANT
Define os tipos das variáveis e as propriedades matemáticas estáticas que devem ser sempre verdadeiras
INICIALIZATION
Define os valores de partida das variáveis por atribuição paralela/simultânea
OPERATIONS
Interface de interação do componente com o usuário ou sistema
Assinatura: Parâmetros de entrada e saída
Precondition: Condições lógicas obrigatórias para que a operação possa ser executada com segurança
Corpo da Ação: Substituições lógicas e alterações de estado executadas simultaneamente
Consistencia de Máquina
Viabilidade do Invariante (Feasibility)
Provar que existe pelo menos um estado matematicamente real que satisfaça o invariante
Consistência da Inicialização
Provar que o estado inicial gerado respeita obrigatoriamente as regras do invariante
Consistência das Operações
Provar que se o invariante e a pré-condição são verdadeiros antes da operação, o invariante continuará verdadeiro após a sua execução
Operações de Consulta
Apenas retornam saídas sem alterar o estado físico; são inerentemente consistentes
Bwm-Definido
Provas adicionais que garantem expressões matemáticas seguras
Causas de Inconsistência
Pré-condição Fraca
Permite disparar a operação em estados inválidos, quebrando o invariante
Operação Incorreta
Erro lógico no corpo/ação da operação
Invariante Incorreto
Regras restritivas demais (invariante forte que exclui estados válidos) ou frouxas demais