SAT SOLVER

• Exemplo 1
• Exemplo 2
• Exemplo 3

ALLOY

Para toda a ação:

• guarda → Condição inicial para a ação poder ser executada
• efeito → Efeito da ação
• frame conditions → Indicar quando algo não muda, sem isso, essa var seria imutável e podia mudar quando quisesse
• reservations.als
• Diferença entre a modelagem estrutural e comportamental
• Modelação Estrutural
• Modelação Comportamental

WHY3

Axioma:

• Definição: Um axioma é uma afirmação ou proposição que é aceita como verdadeira sem a necessidade de prova.
• Uso em WHY3: Axiomas são usados para introduzir fatos fundamentais sobre os quais os teoremas e propriedades do sistema são construídos.

Pré-condição e Pós-condição:

• Pré-condição: É uma condição que deve ser verdadeira antes da execução de uma ação ou função.