 |
Métodos Formais de Programação I - 2006/07
|
[ DI/UM ]
|
---|
Ref. |
Dia |
Hora |
Tipo |
Sala |
Cursos |
Docente |
1 |
5.�-feira |
09h00-11h00 |
T |
DI-A2 |
LMCC/LESI |
J.N. Oliveira |
2 |
5.�-feira |
14h00-16h00 |
TP(1) |
DI-0.11 |
LESI/LMCC |
L.S. Barbosa |
- Em qualquer altura: via correio-electrónico,
devendo ser colocado no assunto o `string' MFP-I/0607;
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:
-
- Nota teórica, por prova escrita sem consulta,
de acordo com regulamentação interna em vigor - épocas
normal (1.� ou 2.� chamada),
de recurso ou especial -- 80%
- Avaliação contínua nas aulas práticas e laboratoriais -- 20%
- Métodos formais e controlo de qualidade em `software' .
Ciclo de vida usando métodos formais. Redução do risco e dos custos.
Resolução de problemas por modelação e cálculo.
Requisitos e modelos. Prototipagem e animação. Validação por teste.
Não-determinismo e parcialidade. Necessidade de modelar com relações.
Relação (especificação) versus função (implementação).
- Linguagens e métodos para especificação formal.
Estudo do `standard' ISO/IEC 13817-1 (VDM-SL).
Especificação por pré/pós-condições. Invariantes.
Sub-especificação e não-determinismo.
Modelação por conjuntos, sequências e funções finitas.
- Introdução ao cálculo de relações.
Combinadores relacionais básicos.
Taxonomia de relações binárias.
Ordens.
Estruturação do cálculo relacional com base em conecções de Galois.
Formulação de propriedades em notação ``pointfree''.
O cálculo funcional como caso particular.
- Semântica relacional da notação VDM-SL.
Significado de um modelo VDM-SL.
Semântica relacional de um par pre-/post-.
Relações em compreensão. ``Mappings'' e suas propriedades.
- Invariantes.
Significado de um invariante em VDM-SL.
Prova de preservação de um invariante.
Noção de precondição mais fraca que garante uma propriedade.
Exemplos.
A integridade-referencial como uma classe de invariantes sobre
relações simples e finitas em bases de dados.
Diagramas Entidades-Relações (ER) e sua semântica
pointfree baseada na preordem de definição de relações.
- Especificação indutiva.
Estratégia de divide-and-conquer
e sua captação sob a forma de um hilomorfismo relacional.
Cálculo de pontos-fixos.
Notação �.
Teorema da fusão-�. Aplicações:
os tipos colectivos de dados em VDM-SLe seus hilomorfismos.
- Prototipagem e animação.
Casos de estudo laboratorial.
Ambientes de desenvolvimento formal.
Experiência com a utilização do ambiente VDMTOOLS -
for Quality Software on Schedule da CSK.
Objectificação: evolução de um modelo VDM-SL para VDM++)
- A especificação formal como método de controlo de qualidade em `software'
Motivação: especificação formal -- porquê e para quê?
Introdução ao binómio especificação /implementação.
Adopção do `standard' ISO/IEC 13817-1 (VDM-SL).
Ciclo de vida do desenvolvimento formal de `software' .
Áreas típicas de aplicação. Sistemas críticos e confiáveis.
Especificação formal construtiva. Modelação de um problema. Prototipagem
e animação. Validação por teste. Importância da verificação formal das propriedades de um modelo.
Não-determinismo e parcialidade. Necessidade de modelar com relações.
- Introdução ao cálculo de relações.
Inclusão de relações. Composição e intersecção de relações.
Monotonia da composição:
Conversa de uma relação e a propriedade de contravariância.
Ordens e sua taxonomia.
As funções vistas como casos particulares de relações.
- O cálculo relacional «pointfree».
Formulação de propriedades em notação «pointfree».
Exemplo -- injectividade de uma função f.
Os operadores ker e img.
Relações inteiras (totais), sobrejectivas e simples (funcionais).
Taxonomia de relações binárias.
A igualdade entre relações, «pointwise» e «pointfree»:
a inclusão cíclica (vulg «ping-pong») e a igualdade indirecta. Igualdade de funções.
Transformada-PF.
Representação de predicados unários (conjuntos) por coreflexivas ou por condições.
Estruturação do cálculo relacional com base em conecções de Galois (CG).
Quadro das principais CG do cálculo relacional.
As propriedades básicas de uma CG intuídas a partir de um exemplo da aritmética.
Exemplos: converso, regras de «shunting», divisão relacional. Intersecção e união.
Versões relacionais de <R,S> e [R,S] como conecções de Galois.
Definição de uma relação.
Domínio e contradomínio como conecções de Galois.
- Semântica relacional da notação VDM-SL.
Significado de uma especificação via pré/pós-condições em VDM-SL.
Semântica relacional de um par pre- / post-:
Spec =Post · Pre .
Papel da pre-condição.
Relações em compreensão. Relações simples finitas e sua representação
em VDM-SL(«mappings»).
Uso do operador ker f em pós-condições para especificar relações de equivalência.
Exemplo: isPermutation = ker seq2bag.
Semântica relacional dos operadores de VDM-SL.
Versão relacional do condicional de McCarthy e sua utilização
na semântica do operador de sobreposição de funções parciais finitas.
- Cálculo de propriedades em VDM-SL.
Significado informal de um invariante em VDM-SL.
Sintaxe VDM-SLpara invariantes.
Exemplos de invariantes e sua relação com as regras de negócio dos sistemas de informação.
Obrigações de prova associadas à formulação de invariantes e pares pré/pós-condição Spec = (pre,post):
(a) satisfabilidade e sua transformada-PF;
(b) preservação de invariantes e sua transformada-PF.
Caso particular em que Spec é uma função.
Necessidade de leis de cálculo-PF para realizar estas provas.
Noção de invariante como tipo.
- Aplicações.
A integridade-referencial como uma classe de invariantes sobre
relações simples e finitas em bases de dados.
Diagramas Entidades-Relações (ER) e sua semântica
pointfree baseada na
preordem de definição de relações.
Exemplos: relacionamentos M:M e M:1.
Diagramas ER e sua semântica relacional (conclusão):
Relacionamentos 1:1.
Preservação de integridade referencial.
- Prototipagem e animação.
Ambientes de desenvolvimento formal.
Casos de estudo laboratorial.
Experiência com a utilização do ambiente
- for Quality Software on Schedule da CSK.
- Informação sobre VDMTOOLS :
entrar em www.vdmbook.com/tools.php, onde uma versão livre está disponível para Windows
- 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.
- Ol06
-
J.N. Oliveira.
Program Design by Calculation.
Draft of textbook in preparation.
Departamento de Informática, Universidade do Minho, 2006.
Bibliografia complementar
|
- F*05
-
John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, and Marcel
Verhoef.
Validated Designs for Object-oriented Systems.
Springer, New York, 2005.
- Ol95d
-
J. N. Oliveira.
Métodos Formais de Programação.
Departamento de Informática, Universidade do Minho, 4.� edição, 1998.
489 p. [mfp.zip]
- Ol99b
-
J.N. Oliveira.
Recursion in the Pointfree Style.
33p., Departamento de Informática, Universidade do Minho, 1999.
- Oli00
-
J.N. Oliveira.
Quasi-inductive datatypes, June 2000.
Departamento de Informática, Universidade do Minho. Chapter of book
in preparation.
- Calendário:
Época
|
Chamada
|
Data
|
Hora
|
Salas
|
Inscritos
|
Prova
|
Normal |
1.� |
2.�-feira, 8-Jan |
09h30 |
2305, 2306 |
26 |
pdf |
Normal |
2.� |
5.�-feira, 25-Jan |
14h00 |
2306 |
25 |
pdf |
Recurso |
- |
6.�-feira, 16-Fev |
09h30 |
1315 |
42 |
pdf |
Especial |
- |
Sábado, 15 de Setembro de 2007 |
09h30 |
1317 |
|
pdf |
[ Informa��o removida (RGPD artigo 17�) ]
Voltar à página principal de MFP-I.
- Outras disciplinas leccionadas pelo DIUM
J. Nuno Oliveira
2007-09-21