Métodos Formais
Preâmbulo
A ciência tem a ver com o perceber-se
como o mundo e as suas coisas funcionam
e a tecnologia com o garantir que
certas coisas que se desejam acontecem
de forma fiável e repetível. A necessidade de basear
a segunda em resultados da primeira é uma constante da evolução das disciplinas
de engenharia, a única de facto capaz de ultrapassar as limitações do
puro experimentalismo e do amadorismo, e de promover a transmissão segura
do conhecimento.
Ora o resultado científico recorre, por natureza, à fórmula matemática
para poder ser expresso e, assim, ser susceptível de raciocínio. É assim
que as engenharias "clássicas", como a civil, a mecânica, a electrotécnica,
a electrónica, etc, recorrem sistematicamente a disciplinas da matemática
(algumas já centenárias) para a arrumação dos seus corpos de conhecimento.
São exemplos conhecidos de todos nós o cálculo diferencial/integral,
a análise numérica, a geometria analítica, etc, etc.
Com o advento das chamadas
Tecnologias da Informação esta situação
alterou-se.
Na verdade,
essas tecnologias desde cedo mostraram alguma dificuldade em sobreviver
sobre tal herança científica,
pelo facto de esta estar demasiado comprometida com a modelização de
entidades da vida real que,
como o
espaço e o
tempo,
são por natureza
contínuas e
infinitas.
Ora o suporte computacional capaz de mecanizar esses modelos é,
por limitação física,
discreto e
finito.
O que faz com que sejam a
matemática discreta, a
lógica formal, a
álgebra universal, etc.
as disciplinas em que o projecto científico do 'software' se alicerça.
Contudo, essas disciplinas encerram uma dificuldade - a de, por serem demasiado
descritivas,
os raciocínios dificilmente escalarem a problemas de
tamanho real.
Existem duas alternativas para sair dessa dificuldade:
apostar em ferramentas de verificação (demonstradores de teoremas, etc) ou apostar em
notações mais económicas e susceptíveis ao raciocínio.
Este módulo segue a segunda destas vias, sendo a sua base o ensino do cálculo de
relações binárias dito 'pointfree' (sem variáveis) e a sua essência a chamada
transformada 'pointfree' que converte expressões da lógica e matemática discreta
como forma de agilizar o raciocínios necessários.
Objectivos
Este módulo estrutura-se, pois, a dois níveis - descrição e cálculo.
No primeiro, ensina-se a especificar 'software' através da criação de
modelos abstractos sobre os quais se pode raciocinar e garantir
propriedades desejáveis ('model-oriented specification'). Ensinam-se várias abordagens à
animação e teste de modelos: o recurso à linguagem funcional
Haskell (equipada com bibliotecas desenvolvidas para esse efeito),
o recurso ao
JML
e as
VDMTools (CSK) que animam o VDM-SL (ISO/IEC standard 13817-1.
No segundo, ensina-se a converter esses modelos para a notação relacional e a raciocinar sobre
eles. O exercício estende-se a outras áreas da modelação como, por exemplo, a formulação de
uma semântica para diagramas ER (entidade-relação), etc.
Pela sua natureza propedêutica, o módulo é central às que a acompanham neste módulo.
A sua articulação com o Projecto Integrado (PI)
é feita ao nível da prototipagem e animação de modelos.
Programa
- Introdução à especificação formal como método de controlo de qualidade em 'software'. Binómio modelação / implementação. Engenharia orientada ao modelo (MDE).
- Ciclo de vida do desenvolvimento formal de 'software'. Especificação formal construtiva. Modelo de um problema. Prototipagem e animação. Validação por teste. Importância da verificação formal das propriedades de um modelo. Obrigações e métodos de prova. Sub-especificação e não-determinismo. Relação (especificação) versus função (implementação).
- Introdução ao cálculo de relações. Inclusão, composição e intersecção de relações. Conversa de uma relação. Formulação de propriedades em notação "pointfree".
- Taxonomia de relações binárias. As funções vistas como casos particulares de relações. Representação de predicados lógicos por relações binárias. Ordens. Estruturação do cálculo relacional com base em conecções de Galois (CG).
- Significado de um invariante. Prova de preservação de um invariante. Noção de precondição mais fraca que garante uma propriedade. Regras para combinação de especificações que satisfazem propriedades.
- A integridade-referencial como uma classe de invariantes sobre relações simples e finitas em bases de dados. Diagramas Entidades-Relações (ERD) e sua semântica pointfree baseada na preordem de definição de relações.
- Uso do Haskell como linguagem de modelação. Invariantes, pre e pós-condições em Haskell. A biblioteca CamilaMonad. Animação de modelos em Haskell.
- Recurso ao JML para anotação formal de código Java.
- O "standard" ISO/IEC 13817-1 (VDM-SL). Significado de um modelo VDM-SL. Semântica relacional de um par pre-/post-. Relações em compreensão. Relações simples finitas e sua representação em VDM-SL ("mappings").
Bibliografia
Departamento de Informática, Universidade do Minho, 2006.
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.