\documentclass[12pt]{article}

\usepackage[T1]{fontenc}
\usepackage[portuges]{babel}
\usepackage{fancyvrb}
\usepackage{a4wide}

\title{Conversão Camila $\longrightarrow$ VDM-SL}
\author{Alberto Manuel B. Simões\\
  {\footnotesize albie@alfarrabio.di.uminho.pt}}
\date{\today\\Departamento de Informática\\ Universidade do Minho}

\parskip .2cm
\begin{document}
\maketitle

\nocite{Barbosa95,Barbosa95a}

\begin{abstract}
  Este documento apresenta o processo desenvolvido para a conversão
  entre duas linguagens de especificação formal: da linguagem Camila\cite{Camila}
  para a notação VDM-SL\cite{VDM,VDM2}. Além da discussão das soluções implementadas,
  discutem-se problemas que não foram possíveis de serem resolvidos
  devido à grande diferença de flexibilidade das duas linguagens.
\end{abstract}


\section{Introdução}
\label{sec:intro}

A linguagem Camila foi desenvolvida no Departamento de Informática
como projecto de investigação e com o intento de desenvolver um
ambiente de prototipagem usando uma linguagem formal. Entretanto, e
impulsionado pelo \emph{standard} VDM, apareceu uma ferramenta
comercial de especificação formal denominada \emph{VDM Tools}. Dado o
grande património de especificações desenvolvidas em Camila,
pretende-se diminuir o trabalho de conversão entre estas linguagens
para que se possa aproveitar toda esta informação.

As seguintes secções apresentam as etapas implementadas no respectivo
conversor.

\section{Reconhecimento da Linguagem}
\label{sec:recling}

Como a tarefa se baseia na conversão entre linguagens, é necessário
reconhecer ou fazer \emph{parsing} ao programa inicial. Aproveitou-se
os analisadores léxico e sintáctico que tinham sido desenvolvidos
inicialmente para o interpretador da linguagem Camila. Este par de
ferramentas constroem uma estrutura em memória que não é mais do que
uma estrutura de árvores generalizadas. Esta estrutura era
inicialmente traduzida directamente para \emph{lisp} que passava a ser
interpretada posteriormente.

Estes ficheiros foram alterados para que se pudesse programar em
\emph{Perl}, e não em \emph{C}. A estrutura gerada em memória
manteve-se com do ponto de vista semântico.

Depois deste processo, qualquer tipo de geração de código (ou mesmo
interpretação) pode ser obtida por travessias desta estrutura. É
exactamente este o processo que é descrito por este documento.

\subsection{Ferramentas Utilizadas}
\label{sec:sec:ferr}

Para efectuar o \textit{parsing} ao código Camila foi usado o
analisador léxico \textsf{C} desenvolvido para a ferramenta original.
Juntou-se-lhe um analisador sintáctico escrito em Perl (usando a
ferramenta \textsf{YAPP} que corresponde a um \textsf{yacc} que gera
Perl). Para permitir a ligação entre o Perl e a linguagem \textsf{C},
utilizou-se uma linguagem de \textit{cola} denominada de
\textsf{XSUB}.

Desta forma, tornou-se possível utilizar a linguagem Perl (bastante
mais flexível) para a conversão entre as linguagens. A programação foi
baseada num sistema de reescrita, reescrevendo estruturas de dados em
código VDM-SL.

Para cada um dos tipos de dados e para cada um dos operadores ou
funções da linguagem Camila, foram construídas funções que os
processam e geram o código correspondente.


\section{Declaração de Tipos}
\label{sec:types}

As declarações de tipos de dados nestas duas linguagens são muito
semelhantes.  Existem, apenas, algumas diferenças de sintaxe e nome de
tipos. Por exemplo:

\begin{center}\begin{tabular}{l|l}
\verb!Camila! & \verb!VDM-SL! \\
\hline
\verb!INT! & \verb!int! \\
\verb!STR! & \verb!seq of char! \\
\verb!X-list! & \verb!seq of X! \\
\verb!X-set! & \verb!set of X! \\
\verb!A -> B! & \verb!map A on B!
\end{tabular}\end{center}

Para este tipo de transformação foi criada uma tabela que mapeia os
tipos Camila e uma função que a escreve em VDM. Sendo esta função
recursiva, torna-se possível a definição de tipos compostos.

Os tipos atómicos são convertidos mediante uma tabela de conversão. Em
relação aos tipos estruturados, a tabela mapeia tipos de dados em
funções que tratam recursivamente os sub-tipos e geram o
correspondente código VDM-SL.

À medida que estes tipos são transformados e definidos, é guardada
informação sobre cada um deles de forma a que posteriormente se
possam saber que tipos de dados existem definidos.

Nesta transformação podemos perder informação relativa a dados
definidos à custa de outros dados, em que estes últimos aparecem após
a definição dos dados anteriores. Exemplo deste problema é o seguinte
código Camila:

%% EXEMPLO DE TIPO DEFINIDO DEPOIS DE SER USADO
\begin{Verbatim}
TYPE
        BAMS = AccId -> Account;
        AccId   = STR;
        AccHolder = STR;
        Amount  = INT;
        Account :: H: AccHolder-set
                   B: Amount
ENDTYPE
\end{Verbatim}
%%

Neste caso, ao ser definido o tipo de dados \texttt{BAMS}, que não
reconhece os tipos \texttt{AccId} e \texttt{Account}, irá construir
uma definição cheia de pontos de interrogação.

\subsection{Invariantes}
\label{sec:data:inv}

A transformação de um invariante Camila num invariante na sintaxe do
VDM-SL resume-se à transformação da função do invariante para a
notação VDM-SL, uma vez que este conceito existe, também, em VDM-SL.
A secção seguinte apresenta a conversão de funções.

\section{Declaração de Funções}
\label{sec:func}

Embora existam várias formas de definição de funções, a estrutura que
o \emph{parser} Camila gera para cada uma delas é muito semelhante o
que permite que sejam tratadas da mesma forma.

Logo na definição da assinatura da função, torna-se imprescindível
distinguir entre funções polimórficas e não polimórficas. A detecção
do tipo de função foi baseada numa tabela de símbolos construída
sempre que um dipo de dados é definido. Desta forma, qualquer tipo que
não tenha sido definido é considerado um tipo polimórfico.

Além da diferença de sintaxe entre a definição de funções polimórficas
e não polimórficas, torna-se apenas necessário indicar variáveis para
os tipos polimórficos. Estas são escolhidas como sendo os nomes dos
tipos desconhecidos.

Para a conversão de funções Camila em funções VDM usou-se a mesma
técnica da conversão de tipos de dados: uma função recursiva que para
cada função ou instrução Camila procura numa tabela um método que a
saiba processar. Dentro deste tipo de conversão foi necessário
construir uma biblioteca para implementar algumas funções em VDM-SL
que existem \emph{built-in} em Camila.

Segue-se um pequeno extracto de pseudo-código que apresenta a
conversão de um \texttt{if} Camila para um \texttt{if} em VDM-SL.

\begin{Verbatim}
  if => sub(condicao, then, else) {

     codigo_condicao = Codigo(condicao)

     codigo_then = Codigo(then);

     if (else) {
       codigo_else = Codigo(else);
       return "if ",codigo_condicao, " then ", codigo_then, " else ", codigo_else
     } else {
       return "if ",codigo_condicao, " then ", codigo_then
     }
  }
\end{Verbatim}

Desta forma, a função trata recursivamente a condição e respectivas
acções de forma a que se torne apenas necessário concatenar os
resultados destas conversões com a sintaxe própria do VDM-SL.

\section{Exemplos}
\label{sec:exemplos}

\subsection{Tipo de dados}

Como primeiro exemplo, apresenta-se a conversão do célebre tipo de
dados BAMS para os tipos de dados VDM-SL. A versão original Camila é:

\begin{Verbatim}
TYPE
        AccId   = STR;
        AccHolder = STR;
        Amount  = INT;
        Account :: H: AccHolder-set
                   B: Amount
        BAMS = AccId -> Account;
ENDTYPE
\end{Verbatim}

que tem uma tradução directa para:

\begin{Verbatim}
types
        AccId = seq of char;

        AccHolder = seq of char;

        Amount = int;

        Account = compose Account of
                H: set of (AccHolder)
                B: Amount
        end;

        BAMS = map (AccId) to (Account);
\end{Verbatim}

\subsection{Polimorfismo}

Este exemplo evidencia a transformação de uma função polimórfica
Camila na sua versão VDM-SL:

\begin{Verbatim}
FUNC intFF2index(ff:A->INT):A-seq 
RETURN
    if ff==[] then <>
    else let (m=intMIN(ran(ff)),
              X={ a | a <- dom(ff): ff[a] == m },
              l=< a | a <- X >)
         in l ^ intFF2index(ff\X);
\end{Verbatim}

\begin{Verbatim}
intFF2index[@A]: (map (@A) to (int)) +> (seq of (@A))
intFF2index(ff) == if ff = { |-> }  
        then [] 
        else let 
        m = intMIN(rng(ff)), 
        X = { a | a in set dom(ff) & ff(a) = m }, 
        l = [ a | a in set X ] in l ^ intFF2index[@A](X <-: ff);
\end{Verbatim}

\subsection{Exemplos de problemas}

Consideremos o seguinte exemplo de função Camila:

\begin{Verbatim}
FUNC ff2STRff(fk:A->B):STR->STR
RETURN let (f=lambda(x).if is-STR(x) then x
                         else if is-INT(x) then itoa(x)
                         else if is-SYM(x) then symstr(x)
                         else "ff2STRfferror")
        in [ f(k) -> f(fk[k]) | k <- dom(fk) ];
\end{Verbatim}

Este exemplo salienta o uso da definição de tipos compostos (incluindo
o próprio tipo \texttt{STR}) polimórficos, de expressões lambda,
algumas funções não implementadas no conversor e construção de
funções finitas por compreensão.

\begin{Verbatim}
ff2STRff[@A,@B]: (map (@A) to (@B)) +> (map (seq of char) to (seq of char))
ff2STRff(fk) == let 
        f = lambda x:?? & if is_(x,seq of char) 
        then x 
        else if is_int(x) 
        then itoa(x) 
        else if is_token(x) 
        then symstr(x) 
        else "ff2STRfferror" in { f(k) |-> f(fk(k)) | k in set dom(fk) };
\end{Verbatim}

Analisando o código gerado é fácil de reparar que estamos perante
código gerado pela falta de indentação. O primeiro problema que se
consegue encontrar neste código é a expressão lambda que não tem tipo
definido para o parâmetro $x$. Posteriormente, encontramos as funções
\texttt{itoa} e \texttt{symstr} que não estão definidas (mas que devem
ser definidas na biblioteca VDM-SL utilizada pela ferramenta de
conversão).

\vskip .5cm

Outro exemplo com problemas é o seguinte:

\begin{Verbatim}
FUNC ffsUNION(s:(A->B)-set):(A->B)-set
RETURN let (ffUnion=plus) in if s=={} then [] else ffUnion-orio([],s);
\end{Verbatim}

Este exemplo mostra mais uma vez a transformação de uma função
polimórfica. Mostra também como a operação \texttt{-orio} é
desmembrada de forma a ser executada em VDM-SL. O seu único problema
reside na detecção do tipo de dados que deve ser passado para a função
\texttt{reduce}.

\begin{Verbatim}
ffsUNION[@A,@B]: (set of (map (@A) to (@B))) +> (set of (map (@A) to (@B)))
ffsUNION(s) == let 
        ffUnion = plus in if s = {} 
        then { |-> }  
        else reduce[](lambda a:int, b:int & ffUnion(a,b),{ |-> } ,s);
\end{Verbatim}

\section{Problemas Encontrados}
\label{sec:probs}

\begin{itemize}
\item Na definição de tipos, caso exista uma definição dependente de
  outro tipo que vai ser definido algumas linhas a baixo, o sistema de
  tipos considera-o polimórfico. Este problema pode ser resolvido
  atravessando a estrutura em memória mais do que uma vez, ou trocando 
  a ordem das declarações no dito código Camila.
  
\item A linguagem Camila é muito mais \emph{lazy} do que a VDM-SL. No
  caso das expressões lambda, a linguagem Camila nunca associa tipos
  de dados aos respectivos argumentos. No caso da linguagem VDM-SL é
  obrigatória a associação de tipos aos argumentos. A ferramenta tenta
  detectar os tipos de dados pelo contexto. No caso de não conseguir
  (a maior parte dos casos) coloca um par de pontos de interrogação.
  
\item Algumas funções não foram implementadas, como o caso do
  \texttt{itoa} e \texttt{symstr}. Uma vez que este tipo de
  funcionalidade não foi encontrada \emph{built-in} em VDM-SL e a sua
  implementação é simples.
  
\item Depois de várias tentativas para usar módulos VDM-SL, não se
  conseguiu utilizar sem ser interactivamente com a \emph{toolbox}
  gráfica, o que não é de todo eficiente para o desenvolvimento de
  software.

\item Por alguma falta de tempo, a conversão de estado Camila para
  estado VDM-SL não foi implementada. No entanto, tudo indica que
  esta será simples de escrever uma vez que o conceito existe em 
  ambas as linguagens.
  

\end{itemize}

\section{Conclusões}
\label{sec:conc}

Devem existir, provavelmente, várias funções que ainda não estejam a
ser transformadas. Isto deve-se ao método de desenvolvimento que se
baseou na tradução de alguns ficheiros de exemplo Camila em VDM-SL. Ou
seja, desenvolvimento orientado ao exemplo.

No entanto, a \emph{framework} está criada e é suficientemente
versátil para ser extendida de forma a converter toda a linguagem
Camila. Em particular, parece-me que teria sido preferível a tradução
de VDM-SL para Camila,optando-se pela implementação mais versátil.

A implementação de um sistema completo de typechecking para o código
Camila poderia possibilitar a detecção de mais alguns tipos nas
expressões lambda.

\subsection{Trabalho Futuro}

No caso de se verificar que esta ferramenta se torna verdadeiramente
útil, será necessária a implementação de estado e a análise exaustiva
de todas as primitivas usadas para verificar se estas se encontram 
contempladas nas tabelas de conversão.

Gostava de pegar nestas duas linguagens, e realizar a transformação
inversa (VDM-SL para Camila) e reescrever/actualizar a linguagem
Camila de forma a lhe introduzir novos operadores, funções e
funcionalidade assim como eliminar outros menos claros, tornando-a
uma linguagem mais documentada e formal.

\bibliographystyle{plain}
\bibliography{bib.bib}

\end{document}
