Especificação e Desenvolvimento Formal de 'Software' - 1998/99
[ DI/UM ]

Ver classificações da disciplina (à data da Época de Recurso) na secção Notas Finais.

Equipa docente

• Teóricas -- J.N. Oliveira (406006)

Horário

5.ª-feira 15h00-17h00 T 0.02 MI/CEI J.N. Oliveira

Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt ), devendo ser colocando no assunto o 'string' EDFS/9899; toda a resposta que tenha interesse geral será aqui afixada numa secção de 'FAQ's, a criar oportunamente.
• Sujeito a marcação verbal pelo docente respectivo, com um mínimo de uma semana de antecedência:

  5.ª-feira 17h00-18h00 MI/CEI J.N. Oliveira

Regime de Avaliação

• Nota teórica, por prova escrita, de acordo com regulamentação interna em vigor.
• Os alunos só poderão fazer melhoria de nota na época de recurso.

Programa Resumido

Está previsto seguir-se de perto o curso da referência [Oli98] abaixo, cf. programa detalhado provisório.

Programa Detalhado

Versão provisória:

1.a Aula (15/10):

     Topics:  . A formal software development "lifecycle"
              . SOUR -- a case study on FM industrial applicaton
              . Program calculation - an overview

2.a Aula (22/10):

     Topics:  . The notation and its background
              . Primitive and derived data structuring constructs
              . An introduction to recursive data structuring

3.a Aula (29/10):

     Topics:  . (Recursive) datatypes are functors
              . Repertoire of implicit, universal and functorial operators
              . Polymorphism as natural transformation

4.a Aula (5/11):

     Topics:  . Introduction to Set-based reasoning
              . The isomorphism subcalculus
              . Examples of application 

5.a Aula (12/11):
     
     Topics:  . Recursive specification revisited
              . The role of functors. Catamorphisms and hylomorphisms

6.a Aula (19/11):
     
     Topics:  . Introduction to the data redundancy subcalculus
              . A refinement target: the relational database model

7.a Aula (26/11):

     Topics:  . Structural abstraction invariant synthesis
              . Examples: linked-lists, a toy bank-account system and a toy
                production database.

8.a Aula ( 3/12):

     Topics:  . Recursive Data Model Reification in SETS
                Recursive Data Model Reification - Examples of Application

9.a Aula (10/12):

     Topics:  . Introduction to hierachical functorial data modelling
              . Coping with 'In loco' Datatype Invariants in SETS
              . The Hash Table Case Study

10.a Aula (17/12):

     Topics:  . Operation Refinement: Merging SETS with other Calculi
              . Program Synthesis by Solving "Reification Diagrams"

11.a Aula ( 7/01):

     Topics:  . Reification of selective update operators
              . CAMILA bams.cam reification laboratory demo.

              . The CAMILA EdiSpec Demo: from language definition as a
                recursive specification exercise to an interactive system.

12.a Aula (14/01):

     Topics:  . Operation Refinement: the "find" operation and
                its generalization to monoidal hylomorphisms
	      . Recursion removal: the linear monadic scheme.
	      . Operation refinement taking local invariants into account.

13.a Aula (suplementar):

     Topics:  . Operation Refinement (conclusion): the PPD "explode" operation
              . CAMILA ppd reification laboratory demo.
              . Pragmatics of SETS: Impact on Relational Database Design
              . Presentation of the CAMILA Toolkit
              . Current Research
              . Final Remarks

Bibliografia

BdM97

R. Bird and O. de Moor.
Algebra of Programming .
Series in Computer Science. Prentice-Hall International, 1997.
C. A. R. Hoare, series editor.

FL98

J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques .
Cambridge University Press, 1st edition, 1998.

Jon86

C. B. Jones.
Systematic Software Development Using VDM .
Series in Computer Science. Prentice-Hall International, 1986.
C. A. R. Hoare.

Oli97

J. N. Oliveira.
Métodos Formais de Programação.
University of Minho, 4.th edition, 1997.
Textbook (489 p. in Portuguese [available as a 846K gzipped PS file]). English version under preparation at the time of writing.

Oli98

J. N. Oliveira.
A data structuring calculus and its application to program development, May 1998.
Lecture Notes of M.Sc. Course (150 p. [available as a 390K gzipped PS file]). Maestria em Ingeneria del Software, Departamento de Informatica, Facultad de Ciencias Fisico-Matematicas y Naturales, Universidad de San Luis, Argentina.

Provas de Avaliação

• Época Normal
  • Prova
• Época de Recurso
  • Prova
• Época Especial
  • Prova

Notas Finais

À data da Época de Recurso:

Nome Curso Classif.

Anália Maria Garcia Lourenço MI 15

Carlos Manuel Pedrosa Moura MI 11

Hugo Amílcar Castelo Pires MI 18

Ilídio Fernando de Castro Oliveira MI 18

Joaquim Jorge Teixeira Gonçalves MI 15

Leonel Domingues Deusdado MI 11

Margarida Maria Apresentação Oliveira MI 13

Marta Henriques Jacinto MI 14

Nelson Manuel Faria Freire MI Faltou

Nuno Gonçalves Rodrigues MI Reprovado

Paulo Noel Rendall Leite de Oliveira Martins MI 12

Vítor Paulo Sequeira Esteves MI 13

António Adriano Cardoso Cambotas CEI Faltou

João Carlos Rodrigues da Rocha CEI Reprovado

João Filipe Brochado Lemos CEI 12

Luís Pedro Madureira Castro e Silva CEI Faltou

Mário Ricardo de Novais Henriques CEI 18

Pedro Miguel Carreira da Maia CEI Faltou

Voltar à página principal de EDFS . Outras disciplinas leccionadas pelo DIUM