Please enable JavaScript.
Coggle requires JavaScript to display documents.
Estruturação e gerenciamento de Projeto no Método B - Coggle Diagram
Estruturação e gerenciamento de Projeto no Método B
Estruturação do Projeto B
Cláusula SEES
Proibição de operações modificadoras
Não transitivo
Acesso a dados em modo leitura
Módulo apátrida: sem variáveis
Grafo de Dependências
Restrição: deve ser estritamente acíclico
Erros: ausência de ordem válida de inicialização
Composto por módulos concertos, imports e sees
Cláusula IMPORTS
Restrito exclusivamente a implementações
Modificação de variáveis via chamadas de operação
Implementação de dados e operações de baixo nível
Exclusividade: variáveis em um único componente
Operações Locais
Especificadas na cláusula local operation
Invariante baseada na tipagem de variáveis
Definição restrita a implementações
Decomposição Funcional
principio de dividir e conquistar para provas simples
Decomposição de algoritmos: redução de instruções por operação
Gerenciamento de complexidade via divisão de componentes
Gerenciamento do Projeto B
Atividades do Projeto
Geração de código: apenas com modelo 100% provado
Modelagem e prova: atividades iterativas e vinculadas
Ciclo de Vida da Prova
Obrigações de Prova falsas
Provas interativas
obrigações de Prova (POs)
Qualidade do Modelo B
Manutenibilidade: limitação do impacto via módulos
Soluções de contorno: simplificação e decomposição
Métrica: máximo de 3000 (POs por componente)
Bibliotecas
Uso: compartilhamento de módulos no workspace
Atualização manual
Conceito: um biblioteca equivale a um projeto B
Workspaces
Gerenciamento: abertura e fechamento flexíveis
Organização: evita duplicação de projetos
Workspace padrão: local