2.2. CAMILA: uma pequena introdução

CAMILA é uma linguagem formal de especificação funcional orientada por modelos algébricos [Jon86] que serve de suporte a um ambiente de prototipagem com o mesmo nome [ABNO97] e que tem as suas origens em duas linguegens de especificação formal: o VDM [Jon86] e o Z [Spi89].

Uma especificação CAMILA é um conjunto de componentes de software. Cada um destes é um modelo composto por um tipo abstracto de dados e por definições de funções e de estado [BA95].

A estrutura geral de um modelo é a seguinte:

          Modelo → MODEL identificador
                    DefTipo
                    DefFunc
                    DefEstado
                    ENDMODEL

DefTipo, a definição de tipo tem a seguinte forma:

           DefTipo → TYPE
                          (id = Tipo)*
                          ENDTYPE

Os tipos básicos do CAMILA são apresentados na tabela seguinte, Tabela 2-1.

Para além destes tipos, o CAMILA tem mais alguns tipos primitivos que não têm uma correspondência matemática directa mas que são inerentes ao seu ambiente de programação.

Na definição seguinte apresenta-se a forma genérica da definição de uma função em CAMILA.

          DefFunc  → FHeader FPreCond FState FBody
          FHeader  → FUNC fid (ParamLst) : typeid
          FPreCond → PRE CondExp
          FState   → STATE exp
          FBody    → RETURNS Exp

Por fim, a definição de um estado faz-se como se mostra a seguir.

          DefEstado → STATE sid : typeid

Para exemplificar estes conceitos apresenta-se o exemplo seguinte:

; ---------- SORTS --------------------
TYPE
   X = ANY;
   Stack = X-list;
ENDTYPE

; ---------- STATE --------------------
STATE  S : Stack;

; ---------- FUNCTIONS ----------------
FUNC push(x:X,s:Stack):Stack
RETURN cons(x,s);
  
FUNC top(s:Stack):X
PRE s != <>
RETURN head(s);

FUNC pop(s:Stack):Stack
PRE s != <>
RETURN tail(s);

; ---------- EVENTS -------------------
FUNC INIT():
STATE S <- <>;
  
FUNC PUSH(x:X):
STATE S <- push(x,S);
  
FUNC POP():X 
PRE  S != <>
RETURN head(S)
STATE S <- tail(S);
  
FUNC TOP():X
PRE  S != <>
RETURN head(S);

A cada tipo CAMILA está associada uma colecção de funções básicas que permitem manusear os valores desse tipo (construir, seleccionar, converter, transformar). Além disso, também estão pré-definidas as conectivas proposicionais e os quantifiadores. Para exemplificar estes operadores, apresentam-se duas tabelas com um resumo das duas colecções de operadores mais usadas ao longo da tese: os operadores para funções finitas e para sequências. Em cada tabela apresenta-se a sintaxe CAMILA e uma breve descrição informal.

As especificações CAMILA podem ser animadas no ambiente de prototipagem designado pelo mesmo nome, CAMILA. Desta maneira, é possível verificar a adequação da especificação ao problema que se está a resolver.