UC2 - Cálculo de Sistemas de Informação

Information Systems by Calculation (E-Learning)

Programa da UC / Course syllabus

  • Métodos formais e qualidade de software. Conceitos básicos: modelo, especificação, verificação e prova.
  • As relações binárias polimórficas como linguagem de especificação formal universal. Setas e diagramas. Estudo do cálculo relacional 'pointfree'. Conexões de Galois. Polimorfismo paramátrico.
  • O papel das funções na taxonomia das relações binárias. Teorema grátis de uma função polimórfica.
  • Atributos e dependências funcionais. O modelo de dados 'pares valores-chave' construído com relações simples, emparelhamentos e coprodutos. Integridade referencial.
  • Preservação de invariantes e satisfação. Cálculo da precondição mais fraca 'wp (f, p)' para uma dada função 'f' e invariante 'p'. Relações (invariantes) como tipos.
  • 'Design by contract' por cálculo apoiado por model-checking.
  • Breve estudo da interpretação abstracta. Funções invariantes. Simulação relacional. Propriedades de segurança e de animação. Redução do espaço de estados por interpretação abstrata.
  • Formal methods for software quality. Basic concepts: model, specification, verification and proof.
  • Polymorphically typed binary relations as a universal formal specification language. Arrows and diagrams. Binary relations in Alloy. Study of the pointfree relational calculus. Galois connections. Parametricity.
  • The role of functions in the taxonomy of binary relations. Relations as types, inc. data type invariants. Theorems for free.
  • Attributes and functional dependencies. Key-value-pair data model = relational simplicity + pairing + coproducts. Referential integrity.
  • Data type invariants: preservation and satisfiability. Calculation of weakest preconditions for invariant preservation.
  • 'Design by contract': combining model-checking with algebraic calculation. Refinement ordering on relations.
  • Brief study of abstract interpretation. Invariant functions. Relational simulation. Safety and liveness properties relationally. Reducing the state space by abstract interpretation.

Bibliografia / Bibliography

  • J.N. Oliveira. Program Design by Calculation. Informatics Department, University of Minho. The chapters that matter for this course in this academic year are the 5th ( 1M), 6th ( 101K) and 7th ( 433K).

Horário / Timetable

Docente Foto Horário Sala
José Nuno Oliveira jno 5a-feira, 14h-17h Sala E7 1.10

NB: poderá haver trocas de horário entre CSI e EM de acordo com necessidades de serviço dos docentes das duas disciplinas.

Alunos

Afonso Rafael Carvalho Sousa A74196 MiEI
Alexandre Miguel Costa Dias A78425 MiEI
Armando João Isaias Ferreira dos Santos A77628 MiEI
Artur Queiroz PG38014 MMC
Diogo Manuel Macedo e Silva A79021 MiEI
Francisco Fernando Vilela Araújo A79821 MiEI
Fábio Rafael Pereira Araújo A78508 MiEI
Gerson Benjamim Hungulu PG35957 MMC
Gonçalo Medeiros São Pedro Raposo A77211 MiEI
Gonçalo Nuno Esteves Duarte A77508 MiEI
Joana Fernandes Cunha PG38929 MEI
Jorge Fernando Alves da Cruz A78895 MiEI
José Carlos do Vale e Sousa A74678 MiEI
João Manuel da Silva Gomes Fernandes PG38930 MEI
Nelson Loureiro PG37020 MMC
Patrícia Filipa Bouça Barreira A79007 MiEI
Pedro Faria Durães da Silva A78434 MiEI
Pedro Henrique Moreira Gomes Fernandes A77377 MiEI
Pedro Miguel Gomes da Silva PG38935 MEI
Ricardo Guerra Leal A75411 MiEI
Tiago André Araújo Monteiro A78961 MiEI

Programa resumido

Introdução aos métodos formais e seu papel na programação. Verificação e cálculo de soluções informáticas. Problemas e sistemas de informação para os resolver. Modelos e seu papel na concepção de soluções. Importância da abstracção na captação de requisitos. Limites da tipagem estática. Papel das relações binárias na modelação formal. Bases de dados seguindo o modelo 'key-value pair'. Taxonomia e álgebra das relações binárias. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy. Demonstração de corrrecção usando álgebra relacional. Noção formal de contrato. Pré-condições mais fracas. Lógica de Hoare em formato relacional.

Regime de avaliação

  • Duas provas de avaliação (mini-teste + teste) e exame de recurso.
  • Avaliação contínua com base em problemas dados nas aulas TP.
  • As provas escritas são de consulta de material impresso, apenas.
  • O mini-teste é eliminatório de matéria para o teste e vale 60%.

Bibliografia adicional

  • C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

Ferramentas

Material

  • Formulário CSI: ( 137K) - Leis do cálculo relacional básico.

  • 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.

  • Biblioteca Haskell: RelCalc.hs - Cálculo relacional básico em Haskell (precisa da biblioteca Cp).

  • Script 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

Enunciados:

Casos de estudo

  • Liga de futebol - modelo em Alloy: liga.als

  • Plano de estudos do MEI - em curso, enunciado: (PDF); modelo Alloy com os quatro invariantes.

Atendimento electrónico (FAQs)

Q01 - Em b ⊥ a ≡ TRUE (página 170 dos apontamentos não devia ser b ⊤ a ≡ TRUE?

R: É uma gralha, obrigado por informar. Aparecerá corrigida na próxima versão desse capítulo. Agradece-se a comunicação de outras gralhas!

Q02 - Tenho uma dúvida na primeira questão do mini teste de 7 de Dezembro 2017. Na cláusula 3, o professor na resolução tem V :E ← V, não deveria ser V :E ← P ?

R: É também uma gralha, que acabo de corrigir. Obrigado por informar.

Q03 - Tentei resolver o exercício 5.45 por igualdade indirecta e não consegui. Muito provavelmente tenho que utilizar a (5.154) mas não consigo ver como.

R: A igualdade c◦ ·(⊤ − c) = ⊥ é equivalente e c◦ ·(⊤−c) ⊆ ⊥. Por (5.151) podemos subir o lado inferior, para c◦ ·(c⇒⊥) ⊆ ⊥. A partir daí aplica-se a (5.154), obtendo-se (c◦ ·c⇒⊥) ⊆ ⊥. Agora é que se pode aplicar a igualdade indirecta para mostrar que c◦ ·c⇒⊥ = ⊥.

Q04 - No exercico 5.24 aplico a definição de injectividade de uma relação seguido da definição de kernel à interseção de R com S, chegando ao ponto (R ∩ S)º . (R ∩ S) contido na identidade. Não sei como hei-de desenvolver o resto da expressão visto que não existe nenhuma fórmula para a composição de interseções.

R: Este é um exemplo em que regras de monotonia ou "thumb rules" ajudam. Veja, por exemplo, como a regra (5.82) o pode ajudar a resolver o exercício.

Q05 - No exercício 5.26 não sei como é que hei-de provar que (⊤.) é um closure operator. Qual é a estratégia?

R: Em (5.97) substitua ⊤ = !º.! e depois use "shunting" e (5.96).

-- JoseNunoOliveira - 15 Sep 2018