CSI/2020-21

Cálculo de Sistemas de Informação

2020/21

Avisos

Atendimento electrónico

• Ver http://tiny.cc/wxn5tz

Programa

• Métodos formais e qualidade de software
  • Conceitos básicos: modelo, especificação, verificação e prova.
• Cálculo relacional básico
  • As relações binárias polimórficas como linguagem de especificação formal universal
  • Taxonomia relacional
  • Combinadores relacionais e suas propriedades.
• Cálculo relacional avançado
  • Conexões de Galois e igualdade indirecta
  • Catamorfismos e hilomorfismos relacionais.
• Aplicações
  • Polimorfismo paramétrico: cálculo de teoremas grátis
  • Lógica de Hoare em formato relacional
  • Modelos de dados relacionais
  • Tipos relacionais e cálculo de invariantes
  • ‘Design by contract’ por cálculo
  • Interpretação abstracta.

Docente e Horário

Docente	Foto	Horário	Sala
José Nuno Oliveira		5a-feira, 13h-16h	CP1 1.21

Alunos

#	Nome	Curso
a83916	Ana João Dias de Almeida	MiEI
a85516	António Manuel Carvalho Gonçalves	MiEI
a82529	Carlos Manuel Marques Afonso	MiEI
a34900	Cecília da Conceição de Oliveira Soares	MiEI
a67683	César Eduardo da Silva Magalhães	MiEI
pg41842	César Hugo Moreira da Silva	MEI
a80970	Davide da Silva Matos	MiEI
a76089	Etienne da Silva Filipe Amado da Costa	MiEI
a85731	Gonçalo José Azevedo Esteves	MiEI
a86617	Gonçalo Pinto Nogueira	MiEI
a81283	Hugo Filipe Oliveira de Sousa Faria	MiEI
a85573	Jorge Gabriel Alves Cerqueira	MiEI
a84776	José Emanuel Silva Rodrigues	MiEI
pg42839	José Gonçalo Macedo Costa	MEI
a84577	José Pedro Oliveira Silva	MiEI
a85954	Luís Mário Macedo Ribeiro	MiEI
a78566	Marcos Daniel Teixeira da Silva	MiEI
a71407	Maurício Zulueta Lima Salgado	MiEI
a82400	Márcio Alexandre Mota Sousa	MiEI
a85700	Pedro Miguel Araújo Costa	MiEI
a84783	Pedro Miguel Borges Rodrigues	MiEI
a86266	Rafael Inácio Lourenço	MiEI
a75411	Ricardo Guerra Leal	MiEI
a81716	Rodolfo António Vieira da Silva	MiEI
a80789	Rui Filipe Brito Azevedo	MiEI
pg36086	Vítor Hugo Gonçalves Silva	MMC

Método de avaliação

• Duas provas escritas de avaliação (mini-teste + teste) e exame de recurso. / 2 written exams
• As provas escritas são de consulta de material impresso. / The exams are open-book
• O mini-teste é eliminatório de matéria para o teste e vale 50%. / The first exam amounts to 50% of the final mark

Classificações

Retiradas para cumprimento do GDPR.

Material Pedagógico

• Formulário

Enunciados de provas de avaliação

• Mini-teste
• Teste
• Recurso

Slides

• Slides da aula de 7-Jan

Casos de estudo

• Mercearia da D. Acácia - queries são paths em diagramas relacionais. (Alloy)
• Liga de futebol - quocientes de funções. (Alloy)
• Sinalização ferroviária - diferença relacional. (Alloy)
• Plano de estudos do MiEI - pré-condições mais fracas; redundância de invariantes.

Código

• Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
• Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.
• Módulo Alloy: prod.als - produtos cartesianos em Alloy.
• Script básica alloy.sed para converter instâncias geradas pelo Alloy para Haskell - em Alloy, visualizar instância em modo Txt e copiar para ficheiro, eg. i.txt; de seguida correr, numa shell, sed -f alloy.sed i.txt

Bibliografia

• J.N. Oliveira. Program Design by Calculation, Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, time permitting).

Outras leituras recomendadas

• D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
• C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

Ferramentas

• Alloy / Electrum (a última versão pode ser encontrada aqui)
• Haskell

Programa detalhado

• Ver http://tiny.cc/wxn5tz