Please enable JavaScript.

Coggle requires JavaScript to display documents.

Lectures - Coggle Diagram

- - - - Animação
      - Transformação
      - Prova de propriedades
    - - Construção
      - Verificação
      - Prova formal
    - - Ao formalizar o sistema a ser desenvolvido força o desenvolvedor a entender os pequenos detalhes do sistema e, com isso, clarificar possíveis ambiguidades
    - - Caso seja possível animar ou executar o comportamento do sistema a partir da especificação permite rapidamente a validação do sistema sem de fato implementar o sistema inteiro
    - - State-based/Modification-based
        
        Definição clara das mudanças executadas por cada operação na modelagem do sistema
        
        Foca na manipulação dos dados, como evoluem e como são relacionados, a linguagem LOTOS é um exemplo
      - Modelos declarativos
        
        Foco no que a solução é de fato, inclui linguagens como PROLOG, Ocaml, Coq, ELAN e linguagens para definições formais da semantica
      - B Method
        
        Desenvolvimento vertical
        
        Correto por construção
        
        O comportamento do sistema pode ser expresso pelo foco nas suas operações, portanto é categorizado como state-based/modification-based
- - - - O objetivo é obter código que esteja de acordo com a especificação do sistema
      - Modelagem
        
        Especificação antes do código
        
        Formalismo matemático
        
        Consistência entre a especificação e o modelo
        
        Sem contradições entre modelo/especificação
        
        Código gerado a partir do modelo
    - - Sem interrupções que modifiquem o estado das variáveis
      - Softwares Multi-Thread podem ser feito usando Event B
    - - Detecção de erros por prova e não por teste
      - Provas são exaustivas, testes não.
      - O software é provado ser livre de erros do programação
    - - Decomposição do programa
        
        O programa se utiliza de outras funções e métodos provados anteriormente
        
        Prova em camadas
        
        A prova é gerenciável conforme a complexidade do sistema é subdividida em cada decomposição
    - - O objetivo é analisar e verificar a especificação a nível de sistema
      - Modelo progressivo
        
        Contém o comportamento do sistema
        
        Significa que o primeiro modelo é simplificado e conforme se desenvolve novos modelos para conter as necessidades do sistema, o modelo no geral vai sendo refinado para estar de acordo com as novas definições
        
        Os refinamentos feitos são provados estarem de acordo com o modelo original e com suas futuras versões
    - - Método orientado a especificação
      - Baseado em linguagem matemática
      - Estruturado
        
        Módulo
        
        Quebra o software em partes menores
        
        Variáveis são implementadas em apenas um único módulo
        
        Contém a especificação e sua implementação
        
        Refinamento
        
        Adiciona detalhes na implementação
        
        Refinamento via dados
        
        O tipo do dado é tornado mais concreto
        
        Refinamento via algoritmo
        
        O processamento é mais explicíto
      - Framework para desenvolvimento validado por prova
    - - Todos os modelos são consistentes e qualquer refinamento está de acordo com a especificação
      - Geração de código é feita traduzindo as implementações para o código fonte
      - O software final é obtido com a junção de todos os códigos fontes gerado mais qualquer outro código a mais que precisou ser escrito e testado
      - Como todo o desenvolvimento do software estará de acordo com a especificação por prova, é poupado muito tempo no desenvolvimento, detectando erros logo no início e evitando erros clássicos de programação (como divisão por 0, overflow, etc)
- - - - Módulos
        
        Componentes
        
        Máquinas abstratas
        
        Contém a especificação do B model
        
        Define o modelo matemático
        
        Abstração da descrição do estado do espaço e seus estados iniciais além da descrição das operações de consulta ou modificação
        
        Refinamentos
        
        Adiciona detalhes na implementação para melhoramento do modelo
        
        Torna o modelo mais concreto
        
        Implementações
        
        O último refinamento
        
        Toda implementação está de acordo com sua especificação
        
        Conformidade é garantida por prova
        
        Aspectos
        
        Dinâmico
        
        initialisation
        
        operations
        
        Obrigações de prova
        
        Garante que as propriedades do aspectos estático são consistentes, são 'ligadas' pela inicialização do aspecto dinâmico e são preservadas por todas as operações
        
        Estático
        
        sets
        
        constants
        
        variables
        
        invariant
        
        Sets, constants e variáveis são referenciados pela definição de suas propriedades estáticas (invariant), inicializados pelo aspecto dinâmico e tem seus estados modificados através das operações
        
        Cada módulo é feito de componentes e são ligados aos outros módulos pela especificação do sistema, seja pelo import ou apenas a visualização do conteúdo de um outro módulo
        
        Cada módulo é responsável por seu próprio espaço de dados
      - Um projeto em B é um conjunto de módulos organizados como uma árvore de tal forma que não gera ciclos
      - Bibliotecas
        
        Outro projeto B pode ser usado como uma espécie de biblioteca para o desenvolvimento do software desejado por meio da chamada de suas funções
        
        Código tradicional pode integrar ou ser integrado no projeto em B
        
        É necessário garantir via testes que o código escrito esteja de acordo com a especificação do sistema