A Linguagem CAMILA  

CAMILA é uma linguagem de especificação formal modular e concorrente, por modelos, actualmente em desenvolvimento na Universidade do Minho.

Uma especificação CAMILA é uma hierarquia de Módulos, que podem, ou não, executar concorrentemente. Um módulo consiste na definição de um conjunto de Tipo de Dados e de Operações (ie. funções com estado). Os tipos de dados são definidos utilizando os tipos básicos:

• INT - Inteiros;
• STR - Strings;
• SYM - o tipo dos Símbolos do XMetoo, pode ser utilizado como Booleano estando definidas as constantes true e false.

• Etiquetação
• Listas
• Conjuntos
• Funções Finitas
• Relações
• Tuplos
• Alternativas

A cada definição de tipo pode estar associado um Invariante, isto é, uma função Booleana que permite restringir os valores do tipo a um subconjunto dos valores tornados possíveis pela sua definição. A definição das operações é feita por duas condições:

• uma pré-condição que expressa quais as relações que devem existir entre os argumentos e entre eles e o estado para que a utilização da operação seja válida;
• uma pós-condição que expressa a relação entre o resultado da operação e/ou o estado depois da sua invocação e os argumentos e estado inicial.

Cada módulo pode receber outros módulos como parâmetros, utilizando as operações e tipos de dados neles definidas para a sua própria definição. Este mecanismo de composição é possível devido à existência do conceito de Interface. Uma Interface pode ser vista como o tipo de um módulo na medida em que contém a declaração dos tipos de dados e operações que um módulo deve definir para que lhe obedeça. Este mecanismo permite também um elevado grau de encapsulamento pois, ao utilizarmos um módulo, temos apenas que nos preocupar com a sua interface, o que permite que a sua implementação/especificação possa ser alterada de um modo completamente transparente.

  
Figure 11: Exemplo de uma Especificação CAMILA

Na figura 11 pode ver-se um extracto de especificação retirado de [Roc91]. Nela, é apresentada a interface de uma Stack e um módulo que a respeita. Na interface são declarados os tipos (sorts) e as operações (events) que o módulo deverá definir, bem como o tipo do estado do módulo. Para cada operação é indicada a sua assinatura (tipos dos seus argumentos e tipo do seu resultado), como todas as operações têm acesso ao estado ele não necessita ser incluído nas assinaturas. O módulo StackAsList especifica uma Stack genérica e obedece à interface anterior. O estado inicial de cada operação é representado por sigma, o estado final por sigma'. O módulo tem um parâmetro E que deverá obedecer à interface ITEM que não é aqui apresentada mas declara apenas a espécie Objecto. Supondo que tínhamos um módulo Integers do tipo ITEM que definia Objecto como INT, podemos escrever uma Stack de inteiros do seguinte modo:

StackAsList(Integers())

Um sistema especificado em CAMILA consiste, do ponto de vista de quem o deve utilizar, no conjunto de operações e tipos de dados da interface do módulo de mais alto nível da especificação. Cada operação tem uma assinatura que deve ser respeitada e a sua utilização só é válida quando a pré-condição a ela associada se verifica.

É com base nesta informação que partimos para a definição do sistema de Geração de Interfaces em Modo Assistido.