Implementering av fargedeteksjon

Os módulos Lexical e Instruction da descrição B0 são utilizados para ilustrar as principais seções e elementos de notação de uma gramática SDF. No módulo Lexical (fig. 5.3) são inseri- das as definições para as estruturas elementares da linguagem. Inicialmente, na seção imports, são referenciados os módulos Identifier, com a definição para os símbolos terminais identifica- dores e Integer, com a definição para os terminais inteiros. Esses elementos foram separados em módulos distintos para que pudessem ser compartilhados como a descrição gramatical para Java. Essa abordagem tornou possível a tradução desses elementos diretamente de uma lin- guagem para outra, sem a necessidade de regras de reescrita intermediárias. Uma vez que os caracteres permitidos aos identificadores em B são um subconjunto daqueles para Java, é pos- sível, no processo de tradução, restringir os identificadores de Java apenas aos permitidos em B.

A priori, para SDF, os terminais da linguagem são simplesmente classes de caracteres, ou seja, sequências de letras ou números. Por outro lado, é possível criar produções para identificar cada token específico, o que é feito na seção lexical syntax do módulo. Na figura 5.3, a produção B-ASTRINGdefine os delimitadores de strings em B. Por sua vez, o símbolo especial LAYOUT corresponde a elementos que devem ser ignorados pelo parser, como comentários, ou aqueles que são inseridos entre os tokens atuando como separadores de símbolos, tais como caracteres de espaço ou de nova linha. Ainda em lexical syntax, vê-se as definições para elementos léxicos da linguagem B, tais como constantes booleanas (TRUE e FALSE) e conjuntos.

As produções da gramática podem ser encontradas nas diversas seções de definição de elementos, além da lexical syntax, tem-se a context-free syntax e seções de declaração de variá- veis. Uma produção tem a forma: <símbolo>+ -> <símbolo> [{atributos+}]?, ou seja, uma lista de símbolos à esquerda, seguida do operador -> e um símbolo à direita seguido de uma lista opcional de atributos entre chaves. Diz-se que o símbolo à direita é definido pelos sím- bolos à esquerda. Por exemplo, na produção “INT” -> SetIntegerB0, o conjunto de caracteres “INT” é um token significativo para a linguagem B0, definindo um tipo de conjunto inteiro

module B−N o t a t i o n / L e x i c a l i m p o r t s Common / I d e n t i f i e r i m p o r t s Common / I n t e g e r h i d d e n s s o r t s A s t e r i s k B−IDENTIFIER e x p o r t s s o r t s B−ASTRING B o o l e a n L i t I n t e g e r L i t S e t I n t e g e r B 0 SetEmpty S e t I n t e g e r L i s t I d e n t ListIdentComma S e l e c t e d I d e n t L i s t S e l e c t e d I d e n t l e x i c a l s y n t a x [ \ " ] ~ [ \ " ] ∗ [ \ " ] −> B−ASTRING [ \ \ t \ r \ n ] −> LAYOUT [ \ ∗ ] −> A s t e r i s k " / ∗ " ( A s t e r i s k | ~ [ \ ∗ ] ) ∗ " ∗ / " −> LAYOUT "FALSE" −> B o o l e a n L i t "TRUE" −> B o o l e a n L i t I n t e g e r L i t e r a l −> I n t e g e r L i t "MAXINT" −> I n t e g e r L i t "MININT" −> I n t e g e r L i t "NAT" −> S e t I n t e g e r B 0 "NAT1" −> S e t I n t e g e r B 0 " INT " −> S e t I n t e g e r B 0 "BOOL" −> S e t I n t e g e r B 0 " {} " −> SetEmpty " INT " −> S e t I n t e g e r "INTEGER" −> S e t I n t e g e r "NAT" −> S e t I n t e g e r "NAT1" −> S e t I n t e g e r "STRING" −> S e t I n t e g e r I n t e g e r L i t e r a l −> I d e n t i f i e r { r e j e c t } I n t e g e r L i t −> I d e n t i f i e r { r e j e c t } S e t I n t e g e r −> I d e n t i f i e r { r e j e c t } S e t I n t e g e r B 0 −> I d e n t i f i e r { r e j e c t } SetEmpty −> I d e n t i f i e r { r e j e c t } B o o l e a n L i t −> I d e n t i f i e r { r e j e c t } c o n t e x t −f r e e s y n t a x I d e n t i f i e r −> L i s t I d e n t " ( " { I d e n t i f i e r " , " }+ " ) " −> L i s t I d e n t { I d e n t i f i e r " , " }+ −> ListIdentComma { I d e n t i f i e r " . " }+ −> S e l e c t e d I d e n t { a v o i d } { S e l e c t e d I d e n t " , " }+ −> L i s t S e l e c t e d I d e n t l e x i c a l r e s t r i c t i o n s A s t e r i s k −/− [ \ / ] " <" −/− [\ −] "<−" −/− [\ −] LAYOUT? −/− [ \ \ t \ r \ n ] LAYOUT? −/− [ \ / ] . [ \ ∗ ]

Figura 5.3: Módulo Lexical da gramática B0 em SDF.

(SetIntegerB0). Os tokens “NAT” e “NAT1” também são conjuntos inteiros.

Na seção context-free syntax são declarados os elementos não-terminais da linguagem sob a forma de produções mais elaboradas que aquelas encontradas na seção lexical syntax. Por exemplo, uma lista de identificadores (ListIdent) é definida como sendo 1 (um) identificador, ou 1 (um) ou mais identificadores separados por vírgula e entre parênteses. Em lexical restrictions aplicam-se restrições para eliminar ambiguidades no reconhecimento de símbolos da gramática. Por exemplo, em LAYOUT? -/- [\ \t \r \n], tem-se que, após o reconhecimento de um símbolo de LAYOUT, não deve seguir-se o reconhecimento de um outro símbolo de separação (\ \t \r \n). O operador “-/-” deve ser lido como “não deve ser seguido por ”.

tos reject e avoid no módulo Lexical. O primeiro é um mecanismo para filtrar certas derivações de um dado símbolo, removendo essas derivações da árvore de parser. Por exemplo, em Se- tIntegerB0 -> Identifier {reject}, rejeita-se o reconhecimento, como identificadores, de uma cadeia de caracteres correspondendo aos conjuntos inteiros B0. Por sua vez, o atributo avoid, juntamente com o atributo prefer, também caracterizam-se como filtros sobre alguma produ- ção. Nesses casos, se a partir de um nó da árvore for necessário fazer uma escolha entre mais de uma derivação, aquela com prefer será a sub-árvore escolhida. Por outro lado, as derivações demarcadas com avoid serão preteridas em relação a outras que não tenham avoid.

Ressalta-se que o módulo Instruction (figura 5.4) contém as produções para as substituições permitidas ao módulo B de implementação, denominadas de instruções. Utiliza-se esse módulo para exemplificar a definição de não-terminais mais elaborados que aqueles encontrados no módulo Lexical. Em sua maioria, as instruções de mais alto nível (InstructionLevel1) podem referenciar uma ou mais instruções internamente na parte THEN da substituição. Instruções mais complexas, como a condicional, podem ser quebradas em mais de uma produção. O caso geral do IF é a produção InstructionIf, definida como um ramo if seguido de zero ou mais elsif’s (ElsifBranch) e opcionalmente por um else (ElseBranch).

5.2 ASF

Enquanto SDF define o aspecto sintático da linguagem, o Abstract Specification Formalism (ASF) ocupa-se do componente semântico, descrito através de regras de reescrita de termos, conforme detalhado na seção 5.2.1. O formalismo denomina-se ASF+SDF devido à estreita ligação entre esses dois componentes, sendo uma especificação ASF composta da sintaxe em SDF estendida com a noção de variáveis e um conjunto de regras de reescrita.

Em verdade, os nós da árvore de parser gerada a partir do SDF são os termos em ASF [Vin05], e produções em SDF são utilizadas como funções no sistema de reescrita de ASF. O resultado da aplicação dessas funções e das regras de reescrita sobre a árvore de parser origi- nal é uma nova árvore, que pode ser manipulada para diversas aplicações, tais como verificação de tipos, análise de código, refatoração, engenharia reversa e transformação de código.

O presente trabalho usa o formalismo ASF+SDF para especificar a transformação de có- digo entre as linguagens B e Java (Java Card). O conjunto de regras de reescrita foi construído de maneira top-down, estabelecendo a tradução de cada elemento da implementação B em seu correspondente na linguagem Java Card.

module B−N o t a t i o n / I n s t r u c t i o n i m p o r t s B−N o t a t i o n / L e x i c a l B−N o t a t i o n / C o n d i t i o n B−N o t a t i o n / Term B−N o t a t i o n / C o n d i t i o n B−N o t a t i o n / P r e d i c a t e e x p o r t s s o r t s I n s t r u c t i o n I n s t r u c t i o n L e v e l 1 I d e n t i t y ( . . . ) I n s t r u c t i o n B l o c k While c o n t e x t −f r e e s y n t a x I n s t r u c t i o n L e v e l 1 −> I n s t r u c t i o n { p r e f e r } I n s t r u c t i o n B l o c k −> I n s t r u c t i o n L e v e l 1 ( . . . ) While −> I n s t r u c t i o n L e v e l 1 "BEGIN" { I n s t r u c t i o n " ; " }+ "END" −> I n s t r u c t i o n B l o c k "VAR" L i s t I d e n t " IN " { I n s t r u c t i o n " ; " }+ "END" −> I n s t r u c t i o n V a r " s k i p " −> I d e n t i t y S e l e c t e d I d e n t ( " ( " ListTermComma " ) " ) ? " : = " Term −> I n s t r u c t i o n B e c o m e s E q u a l S e l e c t e d I d e n t " : = " E x p r T a b l e −> I n s t r u c t i o n B e c o m e s E q u a l S e l e c t e d I d e n t " : = " "BOOL" " ( " C o n d i t i o n " ) " −> I n s t r u c t i o n B e c o m e s E q u a l ( L i s t S e l e c t e d I d e n t "<−−" ) ? S e l e c t e d I d e n t ( " ( " ListTermComma " ) " ) −> I n s t r u c t i o n C a l l u p L i s t S e l e c t e d I d e n t "<−−" S e l e c t e d I d e n t −> I n s t r u c t i o n C a l l u p I f B r a n c h E l s i f B r a n c h ∗ E l s e B r a n c h ? End −> I n s t r u c t i o n I f " IF " C o n d i t i o n "THEN" { I n s t r u c t i o n " ; " }+ −> I f B r a n c h " ELSIF " C o n d i t i o n "THEN" { I n s t r u c t i o n " ; " }+ −> E l s i f B r a n c h "ELSE" { I n s t r u c t i o n " ; " }+ −> E l s e B r a n c h "END" −> End

CaseBranch E i t h e r B r a n c h OrBranch ∗ E l s e B r a n c h End End −> I n s t r u c t i o n C a s e

"CASE" TermSimple "OF" −> C a s e B r a n c h

"EITHER" ListTermSimpleComma "THEN" { I n s t r u c t i o n " ; " }+ −> E i t h e r B r a n c h "OR" ListTermSimpleComma "THEN" { I n s t r u c t i o n " ; " }+ −> OrBranch "WHILE" C o n d i t i o n "DO" { I n s t r u c t i o n " ; " }+

"INVARIANT" C o n d i t i o n "VARIANT" Term "END" −> While

Figura 5.4: Módulo Instruction da gramática B0 em SDF.

Posteriormente, na seção 5.2.2, apresenta-se a estrutura da descrição em ASF e seus principais componentes.