Aula 1/2 (en) 14/02
Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Verificação de programas baseado em sistemas dedutivos. Lógicas de Floyd-Hoare baseadas em pré e pós condições. Correcção parcial e correcção total. Uma linguagem imperativa simples. Asserções e linguagem das condições. Sistema dedutivo para a correcção parcial.

Brief introduction to formal methods.
Deductive program verification. Floyd-Hoare logic based on pre and post conditions. Assertions and logic of conditions. Parcial an d total correctness. A while imperative language. Deductive system of partial correctness.
Bibliografia: Cap. 1 e 2 RSD, Slides,
LICS Cap 4.1-4.3.2 , RSD cap 5.1-5.4
Regras da Lógica de Hoare/ Hoare logic rules
Exercícios: Hoare Logic