Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1)
Horário | Timetable
Alunos | Students
| # | 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 | MEI |
Programa | 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.
|
Regime de avaliação | Assessment
- 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
Bibliografia | Bibliography
- J.N. Oliveira. Program Design by Calculation (
, 2.4Mb), Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, time permitting).
Bibliografia adicional | Other bibliography
- C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)
Ferramentas | Tools
Material | Teaching material
- Módulo Alloy: RelCalc.als
- Cálculo relacional básico em Alloy.
Atendimento electrónico | FAQs
Q01 -
Eu resolvi o exercício 5.1 mas não precisei de usar a lei (5.17). Porque é que essa regra é sugerida?
R: O uso da lei (5.17), para
f=sq e o resto identidades, poupa passos na resolução, que fica praticamente imediata.
Links
TBC
--
JoseNunoOliveira - 28 Sep 2020
