O caso de estudo do segundo trabalho encontra-se aqui(pdf). Para o interesse dos alunos, um pseudo-código (com alguns erros propositados) encontra-se aqui. Os grupos deverão propor de forma faseada soluções para as seguintes tarefas:
Especificar em Uppaal um sistema NGV (Near Gear Velocity) que permita simular o seu funcionamento (à luz da descrição fornecida mais acima).
Especificar algumas propriedades básicas em Uppaal que permitam validar uma escolha cuidadosa de requisitos.
Propor uma implementação básica do sistema usando uma linguagem de programação da escolha do grupo (à imagem do exemplo listado acima). Exemplos de linguagens de programação (com suporte ao paradigma DbC são: C♯, C, WHY-ML, Java, ADA)
Instrumentar o código proposto com contratos.
Propor uma selecção dos contratos e respectiva validação. Espera-se em particular que sejam explorados os contratos ligados à safety da implementação proposta.
Até dia 16 de Dezembro os alunos deverão formar, por iniciativa própria, um grupo de trabalho para o segundo trabalho de Computação Fiável, na modalidade expressa nas aulas (juntar dois grupos do primeiro trabalho para formar um novo grupo). Passada esta data, o regente formará ele próprio os grupos que restarão por definir.
Contaremos com duas pequenas apresentações de alunos de investigação na aula de sexta-feira 9 de Dezembro (Model checking estocástico, Processos de decisão para provas de equivalência de expressões regulares em COQ).
enviar um email ao regente (desousaUUU@UUUdi.ubi.pt, (retire os UUU) ) com o assunto "ComFia: XXXX" em que XXX é o título da dúvida em questão. Qualquer outro formato no assunto arrisca condenar o email ao esquecimento.
8 Material Pedagógico e Referências Bibliográficas
A avaliação contínua mede em termos práticos a aquisição dos conceitos expostos. Como tal é baseada na realização de três exercícios entregue à equipa docente. Alguns exercícios poderão ter uma parte opcional que, se realizada, poderá valorizar a nota do exercício.
Entrega do enunciado do primeiro exercício: semana do 15 de Outubro
Entrega do primeiro exercício: semana do 7 de Novembro
Entrega do enunciado do segundo exercício: semana do 7 de Novembro
Entrega do segundo exercício: semana do 5 de Dezembro
Entrega do enunciado do terceiro exercício: semana do 12 de Dezembro
Entrega do terceiro exercício: semana do 16 de Janeiro
Frequência: Sexta-Feira 13 de Janeiro 2012
Slides do Capítulo 1 do livro; aqui.
Slides do Capítulo 2 do livro : aqui.
em português, e em conjunto com o Capítulo 1: aqui.
Slides do Capítulo 3 do livro : aqui e aqui.
Slides do Capítulo "Definições indutivas" aqui.
Slides do Capítulo COQ: aqui. aqui e aqui.
Slides do Capítulo Verificação de Modelos - UPPAAL: aqui.
Slides do Capítulo Lógica de Hoare: aqui (principal) et aqui(segundário).
Ficha DN-COQ
Ficha indução
Ficha COQ
Exercício COQ por resolver (variante do exercício 13 da Ficha DN-COQ)
Ficha Lógica de Hoare
Ficha UPPAAL
Arquivo com rascunhos de resolução dos exercícios uppaal
Arquivo com enunciados de provas dos anos anteriores
Livro de Apoio [2] (web-site : aqui)
Referências principais [16, 6, 14, 20, 21, 22, 12, 15]
Referências online segundárias (COQ) :
Tutorial de COQ online - nível básico
Tutorial de COQ - nível básico/intermédio (Coq in a Hurry)
Tutorial de COQ - nível intermédio (Tutorial on Recursive Types in Coq)
Certified Programming with Dependent Types, Adam Chlipala
Software Foundations by Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg and Brent Yorgey
Referências segundárias [3, 4, 25, 13, 24, 11, 7, 8, 9, 18, 19, 5, 10, 26, 1, 23, 17]
Teórica Sexta-Feira das 9h00 às 11h00 6.13
Prática Sexta-Feira das 11h00 às 13h00 6.13
Terças e Quintas das 9h00 às 11h00
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.
H.P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–310. Oxford University Press, New York, 1992.
Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Serie. Springer Verlag, 2004. http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html
A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Cambridge University Press, New York, NY, USA, 1996.