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.