Please enable JavaScript.

Coggle requires JavaScript to display documents.

L06_07 - Coggle Diagram

- - - - Tipos
        
        Enumerated
        
        Explicitamente lista os elementos do set
        
        Deferred
        
        Finitos e não vazios
  - - - Tipos
        
        Concrete Constant
        
        Se refere a constants que são direatamente implementáveis
        
        Não precisam de refinamentos
        
        Necessitam de valoração
        
        Abstract Constant
        
        Precisam de refinamento
        
        Não podem ser definidas na implementação
  - - - podem ler sets e constants
    - - podem ver sets, constants e variáveis
  - - - Devem existir valores para os sets e constants que satisfazem as propriedades do modelo
      - Máquinas Milagrosas
        
        São máquinas que possuem contradição em sua definição, por exemplo um número maior e menor que 10 ao mesmo tempo
        
        Como evitar?
        
        cláusula de sessões em uma máquina específica separada
        
        Implementar as máquinas que contém as cláusulas das propriedades previamente
        
        Checador de consistência
        
        Uma máquina separada que possui assertions que provam que as clausulas propostas no invariants da máquina desejada são verdadeiras
- - - - S * T = {(x,y) | x : S & y : T}
        notação x |-> y em B
      - S <-> T = POW(S*T)
        R : S <-> T
    - - R : S <-> T
        o domínio de R é o set contendo todos os elementos de S que são relacionados (Por R) com alguns elementos de T
    - - R : S <-> T
        O range de R é set contendo todos os elementos de T que são relacionados (Por R) com alguns elementos de S
    - - R : S <-> T
        A domain restriction de R sobre U é o set contendo todos os elementos de R nos quais o primeiro elemento do par pertence a U
    - - R : S <-> T
        A domain anti-restriction de R sobre U é o set contendo todos os elementos de R nos quais o primeiro elemento do par não pertence a U
    - - R : S <-> T
        a range restriction de R sobre U é o set contendo todos os elementos de R nos quais o segundo elemento do par pertence a U
    - - R : S <-> T
        a range anti-restriction de R sobre U é o set contendo todos os elementos de R nos quais o segundo elemento do par não pertence a U
    - - R : S <-> T
        A relational image de R sobre U é o set contendo todos os elemento de T que são relacionados (por R) com alguns elementos de U
    - - R : S <-> T
        é o set contendo todos os pares (y,x) tais que (x,y) pertencem a R
    - - R0: S <-> T e R1: T<-> U
        é o set contendo todos os pares (x,z) tais que (x,y) pertence a R0 e (y,z) pertence a R1
    - - R0: S <-> T e R1: T<-> U
        é o set contendo todos os pares (x,y) de R0 tais que x não pertence ao domínio de R1 e todos os pares (x,y) de R1 tais que x pertence ao domínio de R1