Please enable JavaScript.
Coggle requires JavaScript to display documents.
Implementation - Coggle Diagram
Implementation
Estágio final da modelagem em B
Nesta etapa codificamos o modelo em B0, um subconjunto de B
Os componentes na implementação estão relacionados à estrutura dos componentes e seus conjuntos, constantes e variáveis de estado.
Cláusulas como refines, imports, sees e promotes são usadas para estruturar conjuntos e suas propriedades.
B0 Substitution
As substituições B0 incluem atribuições, sequências, alternâncias, substituições de casos, loops, blocos e chamadas de operação.
A substituição em B0 descreve uma mudança no estado de uma máquina. Basicamente, é uma maneira de definir como as variáveis do sistema devem ser atualizadas. Um exemplo de substituição simples seria uma atribuição, como x := x + 1, que incrementa o valor da variável x em 1.
B0 expression
As expressões em B0 são construções que podem ser avaliadas para produzir um valor. Elas podem incluir variáveis, constantes, operadores e funções. Por exemplo, x + y é uma expressão que soma os valores de x e y.
B0 predicate
Predicados em B0 são expressões lógicas que podem ser verdadeiras ou falsas. Eles são usados para especificar condições ou propriedades que devem ser satisfeitas. Um exemplo de predicado seria x > 0, que é verdadeiro se x for maior que zero.
B0 types
INT e derivados
BOOL
NAT e derivados
Loops
Base para o behavior de programas
Deve ter uma invariant para garantir o final do loop e uma variant para a logica do loop
Só pode ser usado nas implementações