2022/23
Esta unidade curricular do 1º semestre do 1º ano do Mestrado em Engenharia Informática da Universidade do Minho tem por objectivo introduzir a utilização dos Métodos Formais na Engenharia de Software.
Os alunos interessados em aprofundar os conhecimentos adquiridos nesta unidade curricular podem optar por frequentar o perfil de Métodos Formais de Programação no 2º semestre.
Programa
- Lógicas para especificação formal
- Lógica proposicional
- Lógica de primeira ordem
- Lógica relacional
- Lógica temporal
- Técnicas de prova automática
- SAT solving para lógica proposicional
- SMT solving para lógica e teorias de primeira ordem
- Model-finding via SAT para lógica relacional
- Bounded model-checking via SAT para lógica temporal
- Concepção formal de software com Alloy
- Modelação estrutural
- Modelação comportamental
- Especificação e Verificação de Programas com Why3
- Linguagem lógica, teorias (biblioteca) e prova
- Linguagem de programas, especificação comportamental, e verificação de correcção
- Desenvolvimento de Software com Why3
Docentes
- Maria João Frade (MJF)
- Alcino Cunha (MAC)
- Jorge Sousa Pinto (JSP)
Avaliação
- Exercícios de avaliação (20%)
- Teste individual (80%)
Os exercícios de avaliação serão propostos no final de algumas aulas teóricas e serão para submeter / realizar na plataforma de e-learning na 6ª feira seguinte.
As notas acima de 18 valores (quer na avaliação contínua quer no exame) terão que ser defendidas através da realização de um pequeno projecto.
Horário
| Tipo | Turno | Horário | Sala |
|---|---|---|---|
| Teórica | 2ª 15h-17h | CP1 0.04 | |
| Teórico-prática | 1 | 4ª 14h-15h | CP2 2.05 |
| Teórico-prática | 2 | 3ª 13h-14h | CP1 0.17 |
| Teórico-prática | 3 | 4ª 15h-16h | CP2 2.05 |
| Teórico-prática | 4 | 4ª 16h-17h | CP2 2.05 |
| Teórico-prática | 5 | 5ª 08h-09h | CP1 0.17 |
Planificação
| # | Data | Docentes | Sumário |
|---|---|---|---|
| 1 | 19 Set | JSP,MJF,MAC | Apresentação da UC. |
| 2 | 26 Set | MJF | Lógica proposicional. SAT solving. |
| 3 | 3 Out | MJF | Lógica de 1ª ordem. Modelação em FOL. |
| 7 Out | MJF | AVALIAÇÃO | |
| 4 | 10 Out | MJF | Formalização de modelos de domínio em FOL. |
| 5 | 17 Out | MAC | Modelação estrutural com Alloy. |
| 6 | 24 Out | MAC | Modelação estrutural com Alloy. Tópicos avançados sobre Alloy. |
| 28 Out | MAC | AVALIAÇÃO | |
| 7 | 31 Out | MAC | Tópicos avançados sobre Alloy. Modelação comportamental com Alloy. |
| 8 | 7 Nov | MAC | Modelação comportamental com Alloy. |
| 11 Nov | MAC | AVALIAÇÃO | |
| 9 | 14 Nov | JSP | Introdução ao Why3. Linguagem lógica e prova. Verificação de programas funcionais |
| 10 | 21 Nov | JSP | Verificação de programas funcionais com Why3 (conclusão). Desenvolvimento de sistemas com estado |
| 11 | 28 Nov | JSP | Desenvolvimento e verificação de sistemas com estado em Why3 |
| 12 | 5 Dez | JSP | Verificação de programas imperativos com Why3. |
| 9 Dez | JSP | AVALIAÇÃO | |
| 13 | 12 Dez | MJF | Teorias de 1ª ordem. SMT solvers. |
| 13 Jan | MAC,MJF,JSP | TESTE | |
| 3 Fev | MAC,MJF,JSP | EXAME |
Exercícios de avaliação
| # | Tópico | Blackboard |
|---|---|---|
| 1 | SAT | 7 Out |
| 2 | Alloy estrutural | 28 Out |
| 3 | Alloy comportamental | 11 Nov |
| 4 | Why3 | 16 Dez |
Material
Slides
- Propositional Logic & SAT Solvers
- First-Order Logic & Modeling with FOL
- Formalizing Domain Models in FOL
- Structural design with Alloy
- Mastering Alloy
- App design with Alloy
- Why3: Verification of Functional Algorithms md pdf
- Why3: State-based Development md pdf
- Why3: Verification of Imperative Algorithms md pdf
- First-Order Theories & SMT Solvers
Exercícios
- SAT solving
- Ficheiros DIMACS CNF
- Colab notebooks: PysatExemplo, Meeting, GraphColoring
- Modelação estrutural com Alloy
- Modelação comportamental com Alloy
- Label (operational principles)
- Todo (behavior and operational principles)
- Email (behavior and operational principles)
- Why3
- Verification of Functional Programs
md
pdf
- Solutions: Map, filter, fold
- Solutions: Binary Trees
- ToDo List . Solution
- Labels . Solution
- ToDo List with Timestamps . Solution
- Verification of Functional Programs
md
pdf
- SMT solving
- Ficheiros SMT-LIB 2
- Colab notebooks: Z3Python, Suduko, Skyscrapers
Exemplos
- Alloy
- Why3
Testes
Bibliografia
- Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
- The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
- Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011).
- Software Abstractions: Logic, Language, and Analysis (revised edition). Daniel Jackson. MIT Press (2012).
- The Essence of Software: Why Concepts Matter for Great Design. Daniel Jackson. Princeton University Press (2021)
- Formal Software Design with Alloy 6. Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo (2021).
Outras leituras recomendadas
- D. Jackson. Alloy: a language and tool for exploring software designs. Commun. ACM 62(9): 66-76 (2019). Também existe um vídeo sobre este artigo que pode ser visto aqui.
- Leslie Lamport. If You’re Not Writing a Program, Don’t Use a Programming Language. Bulletin of the EATCS 125 (2018)
Ferramentas
- SAT solvers
- Alloy
- Why3
- SMT solvers