CSI 17 - 02 Nov 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
-- JoseNunoOliveira - 28 Sep 2020
\ No newline at end of file | |
> > |
META FILEATTACHMENT | attachment="csi20201105.pdf" attr="h" comment="" date="1604313179" name="csi20201105.pdf" path="csi20201105.pdf" size="157438" stream="csi20201105.pdf" user="Main.JoseNunoOliveira" version="1" |
|
|
CSI 16 - 31 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
- 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.
| |
Atendimento electrónico | FAQs |
|
CSI 14 - 29 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
a76089 | Etienne da Silva Filipe Amado da Costa | MiEI |
a85731 | Gonçalo José Azevedo Esteves | MiEI |
a86617 | Gonçalo Pinto Nogueira | MiEI |
| |
< < |
pg42833 | Henrique Manuel Sanches Pereira | MEI |
| |
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 |
| |
< < |
pg42840 | Leandro Filipe Pereira Lima | MEI |
pg42842 | Luís Marques | MEI |
| > > |
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 |
| |
a75411 | Ricardo Guerra Leal | MiEI |
a81716 | Rodolfo António Vieira da Silva | MiEI |
a80789 | Rui Filipe Brito Azevedo | MiEI |
| |
< < |
pg42647 | Valeriy Apostolyuk | MEI |
pg36086 | Vítor Hugo Gonçalves Silva | MMC |
| > > |
pg36086 | Vítor Hugo Gonçalves Silva | MEI |
| |
Programa | Course syllabus |
|
CSI 13 - 23 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | | Atendimento electrónico | FAQs | |
< < | TBC | | | |
< < |
| > > |
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 |
|
CSI 12 - 18 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
pg36086 | Vítor Hugo Gonçalves Silva | MMC |
| |
< < |
| | Programa | Course syllabus
| | Ferramentas | Tools | |
< < | | > > | | |
|
|
CSI 11 - 17 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
a81716 | Rodolfo António Vieira da Silva | MiEI |
a80789 | Rui Filipe Brito Azevedo | MiEI |
pg42647 | Valeriy Apostolyuk | MEI |
| |
< < |
pg36086 | Vítor Hugo Gonçalves Silva | MEI |
| > > |
pg36086 | Vítor Hugo Gonçalves Silva | MMC |
| |
|
|
CSI 10 - 15 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
a81716 | Rodolfo António Vieira da Silva | MiEI |
a80789 | Rui Filipe Brito Azevedo | MiEI |
pg42647 | Valeriy Apostolyuk | MEI |
| |
> > |
pg36086 | Vítor Hugo Gonçalves Silva | MEI |
| |
|
|
CSI 9 - 14 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1)
Horário | Timetable
| |
< < |
| > > |
| |
Alunos | Students | | Regime de avaliação | Assessment | |
< < |
- Duas provas escritas de avaliação (mini-teste + teste) e exame de recurso. | 2 written exams
<-- * Avaliação contínua com base em problemas dados nas aulas TP. | Continuous assessment in the classroom --> | > > | | |
- 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 (
, 1.9Mb), Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, time permitting).
| > > |
- 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 |
|
CSI 7 - 12 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
< < | 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.
|
| | Horário | Timetable
| |
< < |
| > > |
| | | |
< < |
| | Alunos | Students | |
| |
> > | 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 de avaliação (mini-teste + teste) e exame de recurso. | 2 written exams
- Avaliação contínua com base em problemas dados nas aulas TP. | Continuous assessment in the classroom
- As provas escritas são de consulta de material impresso, apenas. | The exams are open-book
| > > |
- Duas provas escritas de avaliação (mini-teste + teste) e exame de recurso. | 2 written exams
<-- * Avaliação contínua com base em problemas dados nas aulas TP. | Continuous assessment in the classroom -->
- 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
|
|
CSI 6 - 11 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
pg42842 | Luís Marques | MEI |
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 |
| |
< < |
pg42647 | Valeriy Apostolyuk | MEI |
| > > |
pg42647 | Valeriy Apostolyuk | MEI |
| |
|
|
CSI 5 - 11 Oct 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | | Alunos | Students | |
< < | TBC | > > |
# | 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 |
pg42833 | Henrique Manuel Sanches Pereira | MEI |
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 |
pg42840 | Leandro Filipe Pereira Lima | MEI |
pg42842 | Luís Marques | MEI |
a78566 | Marcos Daniel Teixeira da Silva | MiEI |
a71407 | Maurício Zulueta Lima Salgado | 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 |
pg42647 | Valeriy Apostolyuk | MEI |
| |
|
|
CSI 4 - 30 Sep 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | |
- 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. | > > | 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. | | Bibliografia | Bibliography | |
< < |
- J.N. Oliveira. Program Design by Calculation (
, 1.9Mb), Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, if time permits). Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta
| > > |
- J.N. Oliveira. Program Design by Calculation (
, 1.9Mb), 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 |
|
CSI 3 - 30 Sep 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
| |
< < | Cálculo de Sistemas de Informação | Information Systems by Calculation | > > | Cálculo de Sistemas de Informação | Information Systems by Calculation (H507R1) | | Programa | Course syllabus | | Horário | Timetable
| |
< < |
| > > |
| |
|
|
CSI 2 - 29 Sep 2020 - Main.JoseNunoOliveira
|
|
META TOPICPARENT | name="WebHome" |
Cálculo de Sistemas de Informação | Information Systems by Calculation
| |
> > | 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.
|
Horário | Timetable
Alunos | Students
TBC
Regime de avaliação | Assessment
- Duas provas de avaliação (mini-teste + teste) e exame de recurso. | 2 written exams
- Avaliação contínua com base em problemas dados nas aulas TP. | Continuous assessment in the classroom
- As provas escritas são de consulta de material impresso, apenas. | 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 (
, 1.9Mb), Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, if time permits). Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta
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
TBC
Atendimento electrónico | FAQs
TBC
Links
TBC | | -- JoseNunoOliveira - 28 Sep 2020 |
|
|
|
 Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
|
|