U.Minho 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

Horário

Dia Hora Tipo Sala Cursos Docente
5.ª-feira 15h00-17h00 T 0.02 MI/CEI J.N. Oliveira

Atendimento

Regime de Avaliação

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

Notas Finais

À data da Época de Recurso:

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

10/6/1999
Jose Nuno Oliveira