CSI/2021-22

Cálculo de Sistemas de Informação

2021/22

Avisos

---

Motivação

Na vida lá fora, tudo parece ser uma relação: relação profissional, relação amorosa, relação numérica, relação internacional, relação familiar, relação …, relação … Como será possível ensinar tudo isso a um sistema de informação sem se estudar a sério o que é uma relação (no sentido formal do termo) e como raciocinar com relações? É esse o principal objectivo desta disciplina.

---

Material Pedagógico

Enunciados das provas de avaliação:

Data	Hora	Local	Curso(s)	Descrição	Enunciado
05-Mai	16h00	E1-1.19	MEI/MMC	1º Teste	PDF com resolução
09-Jun	09h00	E7-1.09	MEI/MMC	2º Teste	PDF com resolução
25-Jun	10h00	E7-1.09	MEI/MMC	Exame de recurso	PDF
25-Jul	14h30	E1-2.17	MEI/MMC	Exame de época especial	PDF

Documentação:

• Slides das aulas até 19-Mai (última aula T) inclusivé.

• Formulário - Leis do cálculo relacional.

Código:

• Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.

• Biblioteca Haskell: RelCalc.hs - Cálculo relacional básico em Haskell (baseia-se em Cp.hs).

• Script 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 fazer, numa shell, sed -f alloy.sed i.txt.

---

Docente e Horário

Docente	Foto	Horário	Sala
José Nuno Oliveira		5ª-feira, 16h-19h (T+TP)	E1-1.19

Atendimento

• Em qualquer altura: via correio electrónico para o docente. (Garantir sempre que “CSI” faz parte do assunto.)
• On-line: por combinação com o docente, via BBCU, Zoom etc
• Presencial: 6ª-feira, 16h-17h, por marcação verbal ou por e-mail com um mínimo de uma semana de antecedência, junto do respectivo docente.

Programa

• Métodos formais e qualidade de software
  • Contexto: o problema da (in)segurança informática.
  • Conceitos básicos: modelo, especificação, verificação e prova.
  • Especificação relacional: “everything in life is a relation…”
• 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
  • Polimorfismo paramétrico: cálculo de teoremas grátis
• Aplicações
  • ‘Design by contract’ por cálculo
  • Lógica de Hoare em formato relacional
  • Tipos relacionais e cálculo de invariantes
  • Modelos de bases de dados relacionais
  • Interpretação abstracta.

---

Alunos e classificações

Por favor entrar aqui

---

Regime de avaliação

• Duas provas escritas de avaliação (testes) + exame de recurso.
• As provas escritas são de consulta de material impresso.

---

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

---