Aula teórica 23

16 janeiro 2007, 10:00 • Maria Paula Antunes Abrantes Gouveia

Cálculo de Hoare: demonstração da correcção parcial de um programa para cálculo do factorial ; esboço da demonstração da correcção parcial de um programa para cálculo do número de elementos positivos de uma lista.

Lógica de Primeira Ordem

11 janeiro 2007, 11:30 • Ricardo Joao Rodrigues Goncalves

Exercícios 2.2.1 c), 2.4 relativo a 1.9 d)(ii), 1.8 k)(ii), 1.8 q)(i) e 1.9 g)(i).

Aula teórica 22

11 janeiro 2007, 10:00 • Maria Paula Antunes Abrantes Gouveia

Lógica para verificação de programas: motivação, propriedades da correcção parcial, terminação e correcção total. Cálculo de Hoare para a correcção parcial: sintaxe, semântica informal e regras de inferência.

Lógica e Teste 4

9 janeiro 2007, 11:30 • Ricardo Joao Rodrigues Goncalves

Exercícios 2.1 a), 2.3 relativo a 1.5 s) e a 1.4 f).

Realização do Teste 4.

Aula teórica 21

9 janeiro 2007, 10:00 • Maria Paula Antunes Abrantes Gouveia

Descrição informal da semântica das fórmulas de 1a ordem com quantificadores. Sistema dedutivo T: regras para os quantificadores; exemplos vários de tableaux.