TP 21/2, 11:00
Não houve aula. Motivo: participação no Simposium Doutoral do DI.
Sumários
T 26/2, 9:00
Apresentação da disciplina, método de avaliação, e bibliografia aconselhada.
Introdução à Semântica das linguagens de programação.
T 28/2, 10:00
Estudo de uma linguagem imperativa simples (LC). Definição de uma máquina abstracta. Conceitos básicos sobre relações de transição. Discussão dos inconvenientes da semântica operacional dada por esta máquina e motivação da abordagem estruturada de Plotkin.
TP 28/2, 11:00
Resolução de um exercício – redução de uma configuração da máquina abstracta para a linguagem imperativa simples (cálculo do factorial de um número).
Discussão da implementação da máquina abstracta em Haskell.
T 5/3, 9:00
Técnicas de prova por indução: indução matemática, indução estrutural, e indução sobre regras de inferência. Prova de equivalência das duas últimas à indução matemática. Exemplificação: estruturas indutivas para as expressões e comandos da linguagem LC; sistema de inferência para a avaliação de expressões de LC.
TP 7/3, 11:00
Resolução de um exercício – transições de uma configuração da Semântica Operacional estrutural para a linguagem imperativa simples (cálculo do factorial de um número). Comparação com o exercício da aula anterior.
Discussão da implementação destas regras de transição em Haskell.
T 12/3, 9:00
Continuação do assunto da aula anterior. Prova de uma propriedade da semântica de transições: carácter determinista da relação de transição. Introdução à semântica de avaliação.
T 14/3, 10:00
Semântica Operacional de Avaliação: apresentação das regras de inferência e sua visão algorítmica. Propriedades. Referência ao "Halting Problem". Prova (por contradição) de não existência de uma derivação para a avaliação de um programa divergente.
TP 14/3, 11:00
Resolução de um exercício – aplicação da semântica de avaliação de uma configuração para a linguagem imperativa simples (cálculo do factorial de um número). Comparação com os exercícios das aulas anteriores.
Discussão da implementação destas regras de avaliação em Haskell.
T 19/3, 9:00
Equivalência das semânticas de transição e de avaliação. Esboço da prova. Propriedades da semântica de avaliação, obtidas automaticamente a partir do resultado de equivalência.
T 21/3, 10:00
Noção de equivalência induzida pela Semântica Operacional de Avaliação: prova de congruência. Exemplos de comandos semanticamente equivalentes. Apresentação de um sistema de tipos para a linguagem imperativa simples: asserções de tipagem e regras de inferência. Discussão sobre a utilidade dos tipos na linguagem. Reinterpretação de propriedades à luz do sistema de tipos.
TP 21/3, 11:00
Resolução de exercícios sobre equivalência semântica de programas da linguagem imperativa simples, e sobre assserções de tipos para expressões e comandos desta linguagem.
T 126/3, 9:00
Não houve aula. Motivo: realização do evento ETAPS'07, cuja comissão de organização o docente integra.
T 28/3, 10:00
Não houve aula. Motivo: realização do evento ETAPS'07, cuja comissão de organização o docente integra.
TP 28/3, 11:00
Não houve aula. Motivo: realização do evento ETAPS'07, cuja comissão de organização o docente integra.
T 11/4, 10:00
Introdução ao estudo da Semântica Axiomática da linguagem imperativa simples. Lógica de Floyd-Hoare. Asserções de correcção parcial. Apresentação das regras de inferência. Linguagem de propriedades lógicas: discussão.
TP 11/4, 11:00
Resolução de exercícios sobre Lógica de Floyd-Hoare. Exercícios simples sobre a utilização do axioma da atribuição e a lei da consequência (fortalecimento de pré-condições). Caso de estudo: prova de correcção do programa para o cálculo do factorial de um número.