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. | 
 Horário / Timetable 
   
NB: poderá haver trocas de horário entre 
CSI e EM de acordo com necessidades de serviço dos docentes das duas disciplinas.
 Alunos / Students 
| # | Nome   | Curso | 
|---|
| a82441 | Alexandre Mendonça Pinho | MIEI | 
| pg40866 | Bruno Manuel Pereira Antunes | MMC | 
| a80453 | Bárbara Andreia Cardoso Ferreira | MIEI | 
| a80564 | Carla Isabel Novais da Cruz | MIEI | 
| a83344 | Eduardo Jorge Lima Pinto Barbosa | MIEI | 
| a82885 | José Augusto Ferreira Alves | MIEI | 
| a78073 | João Costeira Faria Gomes | MIEI | 
| a80397 | João Nuno Alves Lopes | MIEI | 
| a68547 | Lucas Ribeiro Pereira | MIEI | 
| a74036 | Manuel João Curopos Monteiro | MIEI | 
| a82400 | Márcio Alexandre Mota Sousa | MIEI | 
| a82535 | Pedro Mendes Pinto | MIEI | 
| pg41094 | Pedro Rafael Paiva Moura | MEI | 
| a82313 | Pedro Teixeira Gonçalves | MIEI | 
| a75411 | Ricardo Guerra Leal | MIEI | 
| a73577 | Ricardo Ribeiro Pereira | MIEI | 
| a82572 | Sara Maria Barreira Melo | MIEI | 
| a75328 | Tiago João Fernandes Baptista | MIEI | 
 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 50%.
 Bibliografia 
 
-  J.N. Oliveira. Program Design by Calculation ( , 1.9Mb), Departamento de Informática, Universidade do Minho. Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta disciplina no corrente ano lectivo são o quinto, o sexto e o sétimo. , 1.9Mb), Departamento de Informática, Universidade do Minho. Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta disciplina no corrente ano lectivo são o quinto, o sexto e o sétimo.
 Bibliografia adicional 
  
 
-  C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition).  (345 pages) (345 pages)
 Ferramentas 
  
 Material 
 
-  Formulário CSI: ( 137K) - Leis do cálculo relacional básico. 137K) - Leis do cálculo relacional básico.
-  Caso de estudo: ( 127K) - Especificação relacional do calendário de um campeonato de futebol (e sua conversão para Alloy). 127K) - Especificação relacional do calendário de um campeonato de futebol (e sua conversão para Alloy).
-  Caso de estudo: ( 52K) - Especificação relacional do problema da 'merceraria da D. Acácia' (com modelo Alloy). 52K) - Especificação relacional do problema da 'merceraria da D. Acácia' (com modelo Alloy).
-   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 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
-  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).
 Notas finais  
 
a68547 (MIEI)  = 16 ; a73577 (MIEI)  = 10 ; a74036 (MIEI)  = 13 ; a75328 (MIEI)  = 11 ; a75411 (MIEI)  = D ; a77211 (MIEI)  = 11 ; a78073 (MIEI)  = 10 ; a78961 (MIEI)  = 12 ; a80397 (MIEI)  = 12 ; a80453 (MIEI)  = 14 ; a80564 (MIEI)  = 13 ; a82313 (MIEI)  = 15 ; a82400 (MIEI)  = R ; a82441 (MIEI)  = 17 ; a82535 (MIEI)  = D ; a82572 (MIEI)  = 12 ; a82885 (MIEI)  = 11 ; a83344 (MIEI)  = 15 ; pg40866 (MMC)  = 18 ; pg41094 (MMC)  = 14
Enunciados de provas de avaliação:
 
-   Enunciado do mini-teste de 28 de Novembro (com proposta de resolução). Enunciado do mini-teste de 28 de Novembro (com proposta de resolução).
-   Enunciado do teste de 16 de Janeiro (com proposta de resolução). Enunciado do teste de 16 de Janeiro (com proposta de resolução).
 Atendimento electrónico (FAQs) 
Q01 - 
Como é que se deve abordar o exercício 5.22? Parece muito trabalhoso...
R: O que se pede é provar que a composição preserva os 4 critérios principais (injectividade, sobrejectividade, etc). Mas basta provar que preserva a injectividade e sobrejectividade apenas, pois os outros casos derivam desses por (5.34) e (5.35). Vejamos como provar que a composição preserva a injectividade (NB: completar / estudar as justificações). São dadas R e S injectivas:
    (R . S ) é injectiva
 <=> { definição }
   ker (R . S ) ⊆ id
<=> { def kernel }
   ker ( S◦ . R◦ . R . S ) ⊆ id
<= { R injectiva (R◦ . R ⊆ id) por hipótese; regra do ponto-médio B }
   ker ( S◦ . S ) ⊆ id
<= { S injectiva (S◦ . S ⊆ id) por hipótese; regra do ponto-médio B }
   id ⊆ id
<= { trivial }
   true
Q02 - 
Consigo ver que o exercício 5.21 deverá basear-se nas leis (5.62) e (5.63) mas não consigo completar o raciocínio. Como devo prosseguir? 
R: Ou S vai ser simples e R injectiva ou vice-versa. Coloquemos a primeira hipótese:
	(P ∩ Q)·S = (P·S) ∩ (Q·S)
<= { (5.62) }
	P · img S ⊆ P ∨ Q · img S ⊆ Q
<= { img S  ⊆ id por hipótese; regra do ponto-médio B }
	P · id ⊆ P  ∨  S · id ⊆ S
<= { P · id = P  etc }
	true
Agora é só verificar R·(P∩Q) = (R·P)∩(R·Q) para R injectiva, seguindo o mesmo método.
Q03 - 
Na resolução da questão 4 do teste do ano passado há uma altura em que chego a	qualquer coisa como dE . V . i1◦ ⊆ Di . i1◦. Por monotonia da composição (. i1◦) consigo ver que dE . V ⊆ Di implica dE . V . i1◦ ⊆ Di . i1◦. Mas eu preciso que sejam equivalentes. Sugestões?
R: Por 'shunting' de i1◦ do termo inferior para o superior (sem o converso), obtém-se i1◦ . i1 nesse lado. Ora i1◦ . i1 = id pois i1 (e i2) são injecções (funções injectivas, cujo núcleo é id). Basta então 'cortar' i1◦ . i1, não havendo perda da equivalência.
Q04 - 
Não sei como pegar no exercício 5.24...
R: Este tipo de exercícios deve ser abordado usando monotonia ou regras de algibeira como (5.82, 5.83) etc. Exemplo: sabemos que R ∩ S ⊆ R fazendo X := R ∩ S na propriedade (5.58) e simplificando. Vamos supor que R é simples. Como "menor que simples é sempre simples" (5.82) então R ∩ S será simples. Etc para os outros casos.
Q05 - 
Como é que se aplica a igualdade indirecta no exercício 5.46? Não consigo ver como.
R: A igualdade 
c◦ · (⊤ − 
c) = ⊥ é equivalente a 
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⇒⊥ = ⊥.
Q06 - 
Não estou a conseguir fazer a primeira prova do exercício 5.37. Como é que se pega na questão?
R: Ora vejamos:
	[R,S]·[T,U]◦ 
 = { (5.117) }
 	(R·i1◦ ∪ S·i2◦) · [T,U]◦
 = { justificar }
 	 (R·i1◦·[T,U]◦) ∪ (S·i2◦·[T,U]◦)
= { justificar }
 	 R·([T,U]·i1)◦ ∪ S·([T,U]·i2)◦
.... (Agora é só continuar)
Q07 - 
Ao resolver uns exercícios deparei-me com uma dúvida: R◦ × S◦ = (R × S)◦ verifica-se?
R: Sim, verifica-se, como facilmente se prova: ( R × S )◦ = ⟨R·π1,S·π2⟩◦ = (π1◦ · R·π1 ∩ π2◦ · S·π2)◦ = R◦ × S◦
Q08 - 
Consegui resolver a primeira prova do 5.39 mas não estou a conseguir resolver a segunda...
R: Na segunda usam-se as propriedades dos coprodutos. Por exemplo, se se começar por (g+k)◦ . (f + h), como (f + h) = [ i1.f, i2.h],
usa-se fusão-+ (relacional, igual à funcional) e fica-se com [(g◦+k◦).i1.f,(g◦+k◦).i2.h] (onde também se usou 5.123). De seguida obtém-se [i1.g◦.f,i2.k◦.h], que é igual a f/g + h/k.
Q09 - 
No teste, para quem realizar a 2ª parte da matéria, excluindo a matéria do mini-teste, que capítulos sairão?
R: A matéria que foi dada depois do miniteste é a seguinte: secções 5.20, 5.21, 5.24 e capítulo 7.
Q10 - 
Não consigo perceber a justificação ao fundo da página 255.
R: É de esperar, já que a justificação está muito imprecisa. Em geral, as funções constantes são tudo menos injectivas (!). Mas, aqui, o tipo de 
const c é 
1 -> N0 (vejam porquê). Logo, 
const c é injectiva, pois o seu núcleo é de tipo 
1 -> 1 e a maior relação possível nesse tipo é 
id : 1->1. (Agradeço esta dúvida, pois permitiu melhorar já a justificação que irá sair na próxima versão dos apontamentos.)
Q11 - 
Na última questão do teste de 17/18 não consigo justificar o terceiro e o quarto passo.
R: As justificações são as seguintes: 3) teorema grátis de 
swap; 4) (F8), após fazer-se 'shunting' de θº.
Q12 - 
Na questão 6 do teste do ano passado não consigo justificar o segundo passo.
R: Fazendo 'shunting' de 
splitAt da esquerda para a direita em 
splitAt ⊆ ((R* × R*) ← R*) · splitAt ficamos com  
id ⊆ splitAtº .((R* × R*) ← R*) · splitAt. De seguida introduzimos variáveis, eg. 
n e 
n'. Como 
n id n' é 
n=n', uma dessas variáveis desaparece.
Q13 - 
Não sei como justificar o penúltimo passo da questão 7 (segunda parte) do teste de 17/18.
R: Dos quatro termos que estão a ser reunidos, se se isolar 
i1·(R◦·R)·i1◦ ∪ i2·(S·S)·i2◦, verifica-se que essa reunião é 
ker R + ker S por aplicação das leis dos coprodutos (
R+S = [ i1· R, i2· S ] etc).
Q14 - 
Não percebo qual a razão para a cláusula 'injective(const e· (const c)◦)' desaparecer no penúltimo passo da prova sugerida para a questão 7 do teste de 18/19.
R: Uma relação R é injectiva sse 
ker R ⊆ id. Neste caso, 
R = const e· (const c)◦, logo 
ker R = const c . (const e)◦ . const e· (const c)◦ ⊆ id. Se fizermos os 'shuntings' do costume, obtém-se 
ker R ⊆ id ≡ ⊤ ⊆ ⊤, por (6.28).
 Links 
History of Formal Methods - links referidos na primeira aula teórica: 
 
Outros: 
 
-- 
JoseNunoOliveira - 17 Sep 2019