Navegando por Autor "Reis, Leonardo Vieira dos Santos"
Agora exibindo 1 - 8 de 8
Resultados por página
Opções de Ordenação
Item An on-the-fly grammar modification mechanism for composing and defining extensible languages.(2015) Reis, Leonardo Vieira dos Santos; Iorio, Vladimir Oliveira Di; Bigonha, Roberto da SilvaAdaptable Parsing Expression Grammar (APEG) is a formal method for defining the syntax of programming languages. It provides an on-the-fly mechanism to perform modifications of the syntax of the language during parsing time. The primary goal of this dynamic mechanism is the formal specification and the automatic parser generation for extensible languages. In this paper, we show how APEG can be used for the definition of the extensible languages SugarJ and Fortress, clarifying many aspects of the syntax of these languages. We also show that the mechanism for on-the-fly modification of syntax rules can be useful for defining grammars in a modular way, implementing almost all types of language composition in the context of specification of extensible languages.Item Certified derivative-based parsing of regular expressions.(2018) Lopes, Raul Felipe Pimenta; Ribeiro, Rodrigo Geraldo; Figueiredo, Carlos Camarão de; Malaquias, José Romildo; Reis, Leonardo Vieira dos Santos; Ribeiro, Rodrigo GeraldoParsing is pervasive in computing and fundamental in several software artifacts. This dissertation reports the rst step in our ultimate goal: a formally veri ed toolset for parsing regular and context free languages based on derivatives. Speci cally, we describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU Grep has been developed using the certi ed algorithms. Practical experiments conducted using this tool are reported.Item Certified virtual machine-based regular expression parsing.(2019) Delfino, Thales Antônio; Ribeiro, Rodrigo Geraldo; Ribeiro, Rodrigo Geraldo; Malaquias, José Romildo; Reis, Leonardo Vieira dos SantosRegular expressions (REs) are pervasive in computing. We use REs in text editors, string search tools (like GNU-Grep) and lexical analyzers generators. Most of these tools rely on converting REs to its corresponding finite state machine or use REs derivatives for directly parse an input string. In this work, we investigated the suitability of another approach: instead of using derivatives or generating a finite state machine for a given RE, we developed a certified virtual machine-based algorithm (VM) for parsing REs, in such a way that a RE is merely a program executed by the VM over the input string. First, we developed a small-step operational semantics for the algorithm, implemented it in Haskell, tested it using QuickCheck and provided proof sketches of its correctness with respect to RE standard inductive semantics. After that, we developed a big-step operational semantics, an evolution of the small-step one. Unlike the small-step, the bigstep semantics can deal with problematic REs. We showed that the big-step semantics for our VM is also sound and complete with regard to a standard inductive semantics for REs and that the evidence produced by it denotes a valid parsing result. All of our results regarding the big-step semantics are formalized in Coq proof assistant and, from it, we extracted a certified algorithm, which we used to build a RE parsing tool using Haskell programming language. Experiments comparing the efficiency of our algorithm with another Haskell tool are reported.Item Compiling general recursive functions into finite depth pattern matching.(2023) Amaro, Maycon José Jorge; Ribeiro, Rodrigo Geraldo; Ribeiro, Rodrigo Geraldo; Vieira, Bruno Lopes; Reis, Leonardo Vieira dos SantosProgramming languages are popular and diverse, and the convenience of extending or changing the behavior of complex systems is attractive even for the systems with stringent security requirements, which often impose restrictions on the programs. A very common restriction is that the program must terminate, which is very hard to check in general because the Halting Problem is undecidable. In this work, we proposed a technique to unroll recursive programs in functional languages to create terminating versions of them. We prove that our strategy is total and we also formalize term generation and run property- based tests to build confidence that the semantics is preserved through the transformation. This strategy can be used to compile general purpose functional languages to targets such as the eBPF and smart contracts for blockchain networks.Item Uma formalização da lógica modal usando o assistente de provas Coq.(2023) Silveira, Ariel Agne da; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Vasconcellos, Cristiano Damiani; Reis, Leonardo Vieira dos SantosA modelagem de determinados tipos de sistemas computacionais com a lógica clássica possui fatores limitantes. Neste contexto, a apresentação de outros sistemas lógicos, como a lógica modal, e a construção de uma biblioteca para o assistente de provas Coq tem o intuito de auxiliar nesta tarefa e facilitar o uso para a verificação de propriedades de sistemas. A semântica da lógica modal é representada pela semântica dos mundos possíveis, onde existe uma relação de acessibilidade que conecta os mundos de um mo- delo. Diferentes restrições impostas na relação de acessibilidade constroem sistemas da lógica modal que auxiliam na representação de propriedades nas mais diversas áreas de estudo. O desenvolvimento da biblioteca tem como objetivo sustentar a formalização de propriedades de softwares e prová-los em Coq.Item MASLAB : um software interativo de simulação para apoio no ensino de modelagem e análise de sistemas lineares.(2022) Aguiar, Italo Almeida; Ribeiro, Rodrigo Geraldo; Ricco, Rodrigo Augusto; Ribeiro, Rodrigo Geraldo; Ricco, Rodrigo Augusto; Silva, Saul Emanuel Delabrida; Reis, Leonardo Vieira dos SantosSimulações aplicadas no contexto educacional são capazes de prover um considerável apoio no processo de aprendizado de determinada área de conhecimento. Este traba- lho propõe o desenvolvimento de um software de simulação interativo, gratuito e de código aberto para uso educacional no contexto da disciplina de Modelagem e Análise de Sistemas Lineares, nomeado MASLAB. Dentro do escopo da disciplina, MASLAB é capaz de compor e simular graficamente, dentro do escopo da disciplina, variações de cenários definidos pelos usuários, seja por visualização em tempo real ou por visuali- zação de um instante específico. Como forma se de testar as saídas do simulador, a metodologia de validação se propôs a replicar um experimento real por meio de dados previamente amostrados, de modo a se buscar uma proximidade relativa aos dados do experimento original. Por fim, são apresentados os resultados obtidos na replicação vir- tual do experimento real e a análise da proximidade esperada dos resultados obtidos no simulador.Item The design of a verified derivative-based parsing tool for regular expressions.(2021) Cardoso, Elton Máximo; Amaro, Maycon José Jorge; Feitosa, Samuel da Silva; Reis, Leonardo Vieira dos Santos; Bois, André Rauber Du; Ribeiro, Rodrigo GeraldoWe describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.Item The formalization and implementation of Adaptable Parsing Expression Grammars.(2014) Reis, Leonardo Vieira dos Santos; Bigonha, Roberto da Silva; Iorio, Vladimir Oliveira Di; Amorim, Luis Eduardo de SouzaThe term “extensible language” is especially used when a language allows the extension of its own concrete syntax and the definition of the semantics of new constructs. Most popular tools designed for automatic generation of syntactic analysers do not offer any adequate resources for the specification of extensible languages. When used in the implementation of features like syntax macro definitions, these tools usually impose severe restrictions. For example, it may be required that macro definitions and their use reside indifferent files; or it may be impossible to perform the syntax analysis in one single pass. We claim that one of the main reasons for these limitations is the lack of appropriate formal models for the definition of the syntax of extensible languages. This paper presents the design and formal definition of Adaptable Parsing Expression Grammars, an extension to the Parsing Expression Grammar (PEG) model that allows the manipulation of its own production rules during the analysis of an input string. The proposed model compares favourably with similar approaches for the definition of the syntax of extensible languages. An implementation of the model is also presented, simulating the behavior of packrat parsers. Among the challenges for this implementation is the use of attributes and on the fly modifications on the production rules at parse time, features not present in standard PEG. This approach has been used on the definition of a real extensible language, and initial performance tests suggest that the model may work well in practice.