Sumários


TP 21/2, 11:00

Não houve aula. Motivo: participação no Simposium Doutoral do DI.

T 21/2, 10:00

Não houve aula. Motivo: participação no Simposium Doutoral do DI.

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.

T 7/3, 10:00

Semântica Operacional Estrutural de Plotkin: relação de transição. Propriedades.

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.