\documentclass[portuges,a4paper]{article} \usepackage{babel} \usepackage{cam2tex} \usepackage{framed} %\usepackage[latin1]{inputenc} \usepackage[utf8]{inputenc} %\usepackage{fancyvrb} \usepackage{t1enc} \usepackage{aeguill} \def\camila{\textsc{camila}} \def\caixa#1{ \vskip .1cm \fbox{\begin{minipage}{0.95\columnwidth}#1\end{minipage}}\vskip .1cm } \begin{document} \title{Simple Camila notation} \author{José João Dias de Almeida} \date{\today} \maketitle =Construtores de tipos Notação mais usada na construção de tipos: \begin{center} \begin{tabular}{|c|l|} \hline $\jjset{A} $ & \mbox{\emph{conjuntos de A}} \\ %\jjrel{A}{B} & \mbox{\emph{relações binárias}} \\ $\jjff{A}{B}$ & \mbox{\emph{mappings}, correspondências de A para B} \\ $\jjseq{A}$ & \mbox{\emph{sequências de A}}\\ $\jjfunc{A}{B}$ & \mbox{\emph{funções de A para B}}\\ $\jjprod{A}{B}$ & \mbox{\emph{produtos}}\\ $\jjprod{campo1 : A}{campo2 : B}$ & \mbox{\emph{produto} com campos}\\ $\jjalt{A}{B} $ & \mbox{\emph{alternativas}}\\ $\jjany$ & \mbox{\emph{tipo universal}}\\ $\jjnil$ & \mbox{\emph{tipo singular}}\\ \hline \end{tabular} \end{center} A definição de um novo tipo pode incluir um predicado sobre os valores de modo a restrigir o conjunto portador -- \emph{invariante}. Se pretendermos definir um tipo \emph{data}, mesmo na sua versão mais simplificativa, é mais fácil definir um conjunto portador mais amplo (Exemplo produto de três inteiros) e restringir os valores com uma função invariante que verifique a validade do triplo. \_camila{ TYPE data = dia: INT * mes: INT * ano: INT inv(d)= dia(d) >0 /\ dia(d) <= 31 /\ mes(d) >0 /\ mes(d) <= 12 /\ nyavail{...}; ENDTYPE } Algumas funções associadas a tipos: \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ tipo de uma expressão \dotfill \_camila{type(e)} \\ expressão compatível com tipo t \dotfill \_camila{is-t(e)} \end{framed} = Funções --- $\jjfunc{A}{B}$ A linguagem \camila{} dispõem de vários modos de definir funções, podendo estas incluir (ou não) definição de tipos de argumentos e resultado, definição de pre-condição, definição de cláusula de estado. É também possível definir funções anónimas. \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ funções compactas \dotfill \_camila{ f(x) *= y;} funções anónimas \dotfill \_camila{ lambda(x).f(x) } \\ funções com assinatura \\ \_camila{ *func f(x1:t1,x2:t2) : t returns g(x1,x2);} funções com assinatura e pré-condição \\ \_camila{ func f(x1:t1,x2:t2) : t pre p(x1,x2) returns g(x1,x2);} funções com assinatura e estado \\ \_camila{ func f(x1:t1,x2:t2) : t state s <- h(x1,x2,s) returns g(x1,x2);} \end{framed} É possível a definição de funções de ordem superior. =Construtores genéricos usados nas expressões A linguagem \camila{} oferece alguns mecanismos habituais em linguagens de especificação, como sejam as expressões \emph{let} (com pattern matching parcial), expressões condicionais (com pattern matching parcial), \emph{or} de linguagem natural. \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ expressão condicional \dotfill \_camila{ if(c1 -> v1, c2 ->v2, else -> vn)} \\ condicional com pattern matching \dotfill \_camila{ if(v1 is- -> f(h,t) , v2 is-<> -> g , v3 is-{e:s} -> h(e,s) , v4 is-{} -> i, else -> j) } \\ expressão let \dotfill \_camila{ let( a = e1, b = e2 ) in f(a,b) } \\ let com pattern matching \dotfill \_camila{ let( = e ) in f(a,b) } \\ or - ou de linguagem natural \dotfill \_camila{ a or b } \end{framed} O operador \texttt{or} (ou de linguagem natural) não é habitual em linguagens de especificação pelo que carece de uma breve explicação. Este operador (próximo do \emph{ou} de linguagem natural) dá como resultado o primeiro argumento excepto se ele for vazio ou indefinido. É usado como operador binário infixo. \_camila{ Or(exp1,exp2) = if( exp1 == {} -> exp2, exp1 == [] -> exp2, exp1 == <> -> exp2, indefinido(exp1) -> exp2, else -> exp1); } =Booleanos A nível dos booleanos, existe em \camila{} as funções lógicas e quantificadores habituais. \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ Negação \dotfill \_camila{ ~ a } \\ Conjunção \dotfill \_camila{ a /\ b } \\ Disjunção \dotfill \_camila{ a \/ b } \\ Implicação \dotfill \_camila{ a => b } \\ Quantificação universal \dotfill \_camila{ all(x <- setexp : p(x)) } \\ Quantificação existencial \dotfill \_camila{ exist(x <- setexp : p(x)) } \\ Quantificação existencial unário \dotfill \_camila{ exist1(x <- setexp : p(x)) } \end{framed} =Mappings, correspondências --- $\jjff{A}{B}$ As correspondências unívocas dispõem das seguintes funções predefinidas: \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ Enumeração de mappings \dotfill \_camila{ [ a1 -> b1, a2 -> b2 ] } \\ Mappings em compreensão \dotfill \_camila{ [f(a) -> g(a) | a <- setexp]} \\ \mbox{} \hfill \_camila{ [f(a) -> g(a) | a <- setexp /\ p(a) ]} \\ Domínio \dotfill \_camila{ dom(f)} \\ Contra-domínio \dotfill \_camila{ rng(f) } \\ Aplicação \dotfill \_camila{ f[x] } \\ Restrição ao domínio \dotfill \_camila{ f / s} \\ Subtracção ao domínio \dotfill \_camila{ f \ s} \\ Reescrita, reescrever $f$ com $g$ \dotfill \_camila{ f + g} \end{framed} = Sequências --- $\jjseq{A}$ As sequências de um tipo A dispõem das seguintes funções de base: \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ Enumeração de sequências \dotfill \_camila{ < a1 , a2 , nyavail{...}> } \\ Sequências em compreensão \dotfill \_camila{ } \\ \mbox{} \hfill \_camila{ } \\ Head \dotfill \_camila{ head(s)} \\ Tail \dotfill \_camila{ tail(s)} \\ Elemento a partir da posição \dotfill \_camila{s[i]} \\ primeiro elemento \dotfill \_camila{p1(x) } \\ segundo elemento \dotfill \_camila{p2(x) } \\ Concatenação \dotfill\_camila{ s ^ r} \\ Acrescentar elemento \dotfill\_camila{ ^ s} \\ \mbox{} \hfill \_camila{ < x : s > } \\ \mbox{} \hfill \_camila{ s1 ^ s2 ^ nyavail{...} ^ sn } \\ Concatenação distribuída \dotfill\_camila{ CONC(< , nyavail{...} >) } \\ Conjunto dos elementos \dotfill\_camila{ { x | x <- s } } \\ \mbox{} \hfill \_camila{ elems(x) } \\ Índices existentes \dotfill\_camila{ inds(s) } \\ Inversa\dotfill \_camila{ reverse(s) } \\ Comprimento \dotfill \_camila{ length(s) } \\ Ordenação \dotfill\_camila{ sort(s) } \\ Ordenação com função de comparação \dotfill\_camila{ sort2(f,s)} \end{framed} As sequências podem ser heterogéneas (Exemplo $S=\jjseq{\jjany}$). = Conjuntos --- $\jjset{A}$ Os conjuntos dispõem das seguintes funções predefinidas: \begin{framed} \noindent \textbf{Descrição} \hfill \textbf{Notação} \ \ \\ Enumeração de conjuntos \dotfill \_camila{ { a1 , a2 , nyavail{...}} } \\ Conjuntos em compreensão \dotfill \_camila{ {f(a) | a <- setexp}} \\ \mbox{} \hfill \_camila{ {f(a) | a <- setexp /\ p(a)}} \\ Escolha não determinística \dotfill \_camila{ choice(c) } \\ Reunião \dotfill \_camila{ c1 U c2 } \\ Intercepção \dotfill \_camila{ c1 * c2 } \\ Subtração de conjuntos \dotfill \_camila{ c1 - c2 } \\ Pertencer ao conjunto \dotfill \_camila{ e in c } \\ Não pertencer ao conjunto \dotfill \_camila{ e notin c } \\ Cardinal \dotfill \_camila{ # c } \\ União distribuída \dotfill \_camila{ UNION( { {nyavail{...}}, nyavail{...}}) } \\ Ordenação \dotfill \_camila{sort(s)} \\ Ordenação com função de comparação \dotfill \_camila{ sort2(f,s)} \end{framed} Os conjuntos podem ser heterogéneos (Exemplo $S=\jjset{\jjany}$). \end{document}