Material disponível ou a disponibilizar:

Bibliografia

• Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

• C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

• J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer, 2011.

• J.N. Oliveira. Extended static checking by calculation using the pointfree transform. In A. Bove et al., editor, volume 5520 of LNCS, pages 195-251. Springer-Verlag, 2009.

• Christel Baier and Joost-Pieter Katoen. Principles Of Model Checking. MIT Press, 2008.

(A completar ao longo do curso)

Acetatos

• J.N. Oliveira. Data type invariants: starting where (static) type checking stops (32 slides) (last update: Oct-2013)

• J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (35 slides) (last update: Oct-2013)

• Alcino Cunha. Modeling (2013)

• J.N. Oliveira. PF transform: when everything becomes a relation (66 slides) (last update: Oct-2013)

• J.N. Oliveira. PF transform: conditions, coreflexives and design by contract (35 slides) (last update: Nov-2013)

• J.N. Oliveira. Alloy meets the AoP — “Relational thinking” at work (70 slides) (last update: Nov-2013)

• Alcino Cunha. Alloy Under the Hood (2013). Implementação em Haskell da semântica e sistema de tipos: Alloy.hs.

• J.N. Oliveira. “Theorems for free”: a (calculational) introduction (34 slides) (last update: Dec-2013)

• Alcino Cunha. A Perspective on Model Checking (2007).

• J.N. Oliveira. PF-transform: using Galois connections to structure relational algebra (79 slides)

• M.J. Frade. Propositional Logic and SAT solvers.

• M.J. Frade. First-Order Logic and SMT.

• M.J. Frade. SMT Solvers.

• L. S. Barbosa. Software architecture for reactive systems (introduction) (30 slides)

• L. S. Barbosa. _Models and logics for reactive systems _ (46 slides)

• L. S. Barbosa. Introduction to process algebra and the Mu-calculus (54 slides)

• L. S. Barbosa. Time-critical reactive systems 1 (23 slides)

• L. S. Barbosa. Time-critical reactive systems 2 (47 slides)

• L. S. Barbosa. Time-critical reactive systems 3 (32 slides)

• L. S. Barbosa. Coordination (64 slides)

• Three papers on Reo (zip) and modelling exercise Reo (pdf)

• L. S. Barbosa. OPEN TEST (deadline: 11 July 2014).

• Slides J. S. Pinto

• M.J. Frade. Propositions-as-types analogy and the Coq proof assistant. (Coq file: lessonCoq1.v)

• M.J. Frade. Programming and Proving in Coq. (Coq file: lessonCoq2.v)

(A completar ao longo do curso)

Outros textos

• J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.

(A completar ao longo do curso)

Exercícios e formulários

• Exercícios de Alloy.

• Exercícios de CSI.

• Formulário de CSI.

• Exercícios de Coq.

Trabalhos práticos e avaliações de VFS

• Calendário de VFS
• Trabalho sobre Verificação Dedutiva
• Notas do teste laboratorial de Coq
• Notas finais, incluindo testes Frama-C/CBMC e TPs

Exemplos

• Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
• Problema do barqueiro em Alloy:
  • Versão estática.
  • Versão dinâmica, idioma global state, operações especificadas com predicados.
  • Versão dinâmica, idioma local state, operações especificadas com predicados.
  • Versão dinâmica com traços, idioma global state, operações especificadas com predicados.
  • Versão dinâmica com traços, idioma local state, operações especificadas com eventos.
• Algoritmo de exclusão mútua de Peterson:
  • Versão Alloy.
  • Versão SMV.
• Semântica de redes de Petri elementares em Alloy: Versão dinâmica, idioma global state, operações especificadas com predicados.

(A completar ao longo do curso)

Enunciados de provas de avaliação individual

• Teste de CSI (com correcção)
• Exame de recurso de CSI

Divulgação

• Daniel Jackson. Dependable Software by Design. Scientific American, Junho 2006.

• Eric Bouwers, Joost Visser, Arie van Deursen. Getting What You measure. Communications of the ACM (CACM) 55(7):54-59, July 2012.

• J.N. Oliveira. Towards Formal Software Development in VS.NET. MSDN Seminars - 14/16th of May, 2002, Porto & Lisbon.

• Leslie Lamport. Why We Should Build Software Like We Build Houses. Wired, 2013.

Ferramentas

• Alloy Analyzer
• NuSMV
• SPIN
• Frama-C
• Uppaal
• SMT-LIB - The Satisfiability Modulo Theories Library
• SATLIB - The Satisfiability Library
• The Coq Proof Assistant
• VDM/Overture

Repositórios

• Repositório de ferramentas da associação FME.
• Repositório de padrões de especificação de lógica temporal.

Atendimento electrónico (FAQs)

(Esta secção será actualizada regularmente com as dúvidas mais frequentes que forem colocadas à equipa docente.)

Q1 - (CSI) Não percebi bem a parte final da resolução do exercício 29 feito hoje na aula: para mim, o "sinal maior ou igual" deveria ser "menor ou igual".

R: Vejamos - ter-se-á:

(∀ s,n : s (S . ≤º) n : s (T . S) n)

== { 2 x (41) }

(∀ s,n : (∃ n':: s S n' ∧ n' ≤º n) : (∃ s':: s T s' ∧ s' S n))

== { ≥º = ≤ ; s T s' = true }

(∀ s,n : (∃ n':: s S n' ∧ n' ≥ n) : (∃ s':: s' S n))

O que quer dizer: Se s é o aluno com número n' e n' é maior do que n, então há um aluno s' com o número n (isto é: a alocação de números a alunos é sequencial).

---

Q2 - (CSI) Tenho dificuldade em decorar a diferença entre núcleo e imagem de uma relação. Há alguma mnemónica que possa ajudar?

R: Haverá concerteza muitas, por exemplo: decore o nome feminino "NEIDE" e leia-o como o acrónimo de "Núcleo, Esquerda, Imagem, Direita, Etc", isto abreviatura de "num núcleo Rº.R o converso está à esqerda, numa imagem R.Rº está à direita, etc". Haverá melhores, mas este já pode ajudar.

---

Q3 - (CSI) A definição de ordem linear na wikipedia é que são relações transitivas, anti-simétricas e "connected" mas pelo gráfico que nos deu nas aulas são também reflexivas. Qual das duas é a definição correcta?

R: Sendo R "connected" tem-se R ∪ Rº = ⊤ e portanto id ⊆ R ∪ Rº pois id ⊆ ⊤ e ⊤ ⊆ R ∪ Rº.

Ora id ⊆ R ∪ Rº é a mesma coisa que id ∩ (R ∪ Rº) = id e que (por distributividade e conversos) id ∩ R = id, o mesmo que id ⊆ R; logo R é reflexiva.

Em suma, "connected" implica "reflexive", logo não é necessário dizer que é reflexiva.

Usa-se muitas vezes o símbolo ≤ para designar uma ordem linear e o símbolo < para designar ≤ - id, a que se chama a (sub)ordem linear estrita de ≤.

---

Q4 - Se eu tiver <∀ a,b : a X b : a=b> posso trocar para <∀ a,b : a=b : aXb> e depois aplicar 'one point', correcto?

R: Não (!) Isso é se o quantificador for o existencial (∃). No caso do universal, a troca possível é de <∀ a,b : a X b : a=b> para <∀ a,b :: a X b => a=b>, cf. a regra (7) dos slides para R = true

---

Q5 - (CSI) A preencher.

R: A preencher.

---

-- JoseNunoOliveira - 11 Sep 2013