Cálculo de Sistemas de Informação

O objectivo deste módulo é mostrar como, de modelos abstractos, puramente declarativos, como os que se estudaram em Métodos Formais , se podem inferir aplicações reais, implementadas em arquitectura cliente-servidor, com garantia de correcção por cálculo.

No plano operacional, aborda-se a derivação de máquinas de estados abstractas (ASM, vulg. objectos) que prestam serviços através de uma API pública a partir dos modelos declarativos estudados em Métodos Formais, por factorização do seu estado interno. Esta derivação designa-se objectificação e obdece a regras precisas.

Passa-se de seguida ao estudo do refinamento de tais ASMs, que se processa aos dois níveis do serviço que prestam: dataware e middleware. Ao primeiro nível, é dada particular ênfase a um cálculo de estruturas de dados que decorre do cálculo de relações binárias estudado anteriormente e que, em particular, substitui o cálculo de normalização de bases de dados relacionais. O uso do referido cálculo é apoiado por uma ferramenta (2LT) desenvolvida localmente e que calcula modelos de dados concretos em SQL a partir de modelos abstractos em Haskell. Ao segundo nível, estuda-se como calcular o código dos métodos (eg. em C/C++, Java, etc) a partir dos respectivos modelos abstractos e com base na ordem de refinamento que introduz definição e determinismo.

No plano prático (e através de um trabalho laboratorial de grupo) o módulo articula com PI (Projecto Integrado) na medida em que se pede aos alunos que desenvolvam protótipos de ASMs em arquitectura cliente-servidor, parte da qual fica em fase de protótipo e a outra é implementada numa plataforma de desenvolvimento, em articulação com Processos e Arquitectura de Software (PAS). Tal prototipagem beneficia, por sua vez, das técnicas estudadas no semestre anterior em Análise e Teste de Software (ATS).

Programa

• Cálculo de refinamento formal de dados. Noção de impedância entre formatos de dados. Princípio da representação de dados. Relações de abstracção e de representação. Inequações de refinamento. Teorema de desrecursivação genérica. Relações de pertença estrutural e acessibilidade estrutural. Implementação de tipos indutivos polinomais em linguagens com gestão de memória dinâmica: Introdução de apontadores em linguagens tipo C/C++. Representação orientada a objectos.

• Cálculo de refinamento algorítmico. A eficiência como principal motivação para o refinamento algorítmico. Fases do refinamento algorítmico: simulação, redução do não-determinismo, mudança de estrutura de dados virtual. Lei de refinamento funcional. Lei de refinamento relacional. Leis de fusão "vertical" e "horizontal". Lei de refinamento de simultâneo de dados e algoritmos. Cálculo de ciclos while como hilomorfismos.

• Prototipagem rápida e integração com outras tecnologias. Integração de protótipos reactivos em arquitecturas cliente-servidor. Emulação de serviços intermédios ("middleware") e de serviços de dados ("dataware").