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").