Please enable JavaScript.

Coggle requires JavaScript to display documents.

MAPA MENTAL L06 E L07, ou - Coggle Diagram

- - - - S * T = {(x, y) | x : S & y : T}
  - - - R: S <-> T
      - Set que contem todos os elementos de S e são relacionados, pela relação R com alguns elemento de T
      - Dom(r) = {x | x : S & #y, (y : T x |-> y : R)}
- - - - Valores estão escondidos, não precisam ser declarados; implicitos
- - - - A maquina precisa suprir essas propriedades
    - - Invariants
        
        Vê
        
        Sets & constants
        
        Vê
        
        Variables
      - Properties
        
        Vê
      - Assertions
      - Inicialização
      - Operações
- - - - Garantir
        
        Usar session clause em uma maquina separada especifica
        
        Implementar as maquinas que tem tais clasulas antes de seguir a implementar as proximas
      - Devem existir valores para os conjuntos e as constantes definidos em priopriedades
  - - - B => ∃ v.l
  - - - B => [T] I
  - - - B & I & P => [ S ] I