Orientador também citado por: CASTOR FILHO, Fernando / Submitted by Rafael Santana (rafael.silvasantana@ufpe.br) on 2017-05-04T19:07:33Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) dissertacao-final.pdf: 950190 bytes, checksum: 71ffd939c48d9c920666a09a05dc0c53 (MD5) / Made available in DSpace on 2017-05-04T19:07:33Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) dissertacao-final.pdf: 950190 bytes, checksum: 71ffd939c48d9c920666a09a05dc0c53 (MD5) Previous issue date: 2016-09-06 / Energy-efficiency has concerned hardware and low-level software designers for years. However, the rapid proliferation of battery-powered mobile devices combined with the growing worldwide movement towards sustainability have caused developers and researchers to study the energy impact of application software in execution. Recent work has studied the effect that factors such as code obfuscation, object-oriented refactorings, and data types have on energy efficiency. In this work, we attempt to shed light on the energy behavior of concurrent programs written in a purely functional language, Haskell. We conducted an empirical study to assess the performance and energy behavior of three different thread management approaches and three primitives for concurrency control using nine different benchmarks with an experimental space exploration of more than 400 configurations. In this study, we found out that small changes can make a big difference in terms of energy consumption. For instance, in one of our benchmarks, under a specific configuration, choosing one concurrency control primitive (MVar) over another (TMVar) can yield 60% energy savings. Also, the relationship between energy consumption and performance is not always clear. We found scenarios where the configuration with the best performance also exhibited the worst energy consumption. To support developers in better understanding this complex relationship, we have extended two existing performance analysis tools also to collect and present data about energy consumption. In addition, based on the results of our empirical study, we provide a list of guidelines for developers with good practices for writing energy-efficient code in this environment. / Há anos eficiência energética é uma preocupação para designers de hardware e software baixonível. Entretanto, a rápida proliferação de dispositivos móveis alimentados por bateria combinado com o crescente movimento global em busca de sustentabilidade tem motivado desenvolvedores e pesquisadores a estudar o impacto energético de softwares de aplicação em execução. Trabalhos recentes tem estudado o efeito que fatores como obsfucação de código, refatorações em linguagem orientadas à objetos e tipos de dados tem em eficiência energética. Este trabalho tenta lançar luz sobre o comportamento energético de programas concorrentes escritos em uma linguagem puramente funcional, Haskell. Nós conduzimos um estudo empírico para avaliar o desempenho e o comportamento energético de três diferentes abordagens para gerenciamento de threads e três primitivas para controle de concorrência usando nove diferentes benchmarks com um espaço de exploração experimental de mais de 400 configurações. Neste estudo, descobrimos que pequenas mudanças podem fazer uma grande diferença em termos de consumo de energia. Por exemplo, em um dos benchmarks, sob uma configuração específica, escolher uma primitiva de controle de concorrência (MVar) ao invés de outra (TMVar) pode acarretar em uma economia de 60% em consumo de energia. Percebemos também que nem sempre a relação entre consumo de energia e desempenho é clara. Em alguns cenários analisados, a configuração com melhor desempenho também apresentou o pior consumo de energia. Para ajudar desenvolvedores a entender melhor essa complexa relação, nós estendemos duas ferramentas de análise de desempenho existentes para coletar e apresentar dados sobre consumo de energia. Adicionalmente, baseado nos resultados do nosso estudo empírico, listamos um conjunto de recomendações para desenvolvedores com boas práticas de como escrever código energeticamente eficiente nesse ambiente.

Functional purity is a fundamental part of the functional programming paradigm. A function is functionally pure if it is side-effect free and deterministic. Pure functions provide many benefits compared to impure ones, including guaranteed thread-safety as well as easier testing, debugging and maintenance. But how can functional purity be measured? This thesis develops a method for statically measuring the level of functional purity in any given C# program. It also investigates problems with determining purity in object-oriented languages, with a focus on C#. Moreover, a prototype of the method is implemented in order to evaluate the method using a benchmark consisting of 11 open source repositories that use C#'s [Pure] attribute. The [Pure] attribute can be placed in front of a method declaration to indicate that it is side-effect free. Due to a number of limitations to the implementation as well as to [Pure]'s definition of functional purity, which excludes determinism, the results of the evaluation appear relatively poor. After normalizing the implementation's classification distribution for each repository, its classification of pure functions has a precision of 65% and recall 17%, and its classification of impure functions has 54% precision and 69% recall. Nevertheless, the prototype still shows the potential of the full analysis method. A complete implementation of the analysis method could potentially yield a fully working system for measuring any C# program's level of functional purity.

HOLCF is an interactive theorem proving system that uses the mathematics of domain theory to reason about programs written in functional programming languages. This thesis introduces HOLCF '11, a thoroughly revised and extended version of HOLCF that advances the state of the art in program verification: HOLCF '11 can reason about many program definitions that are beyond the scope of other formal proof tools, while providing a high degree of proof automation. The soundness of the system is ensured by adhering to a definitional approach: New constants and types are defined in terms of previous concepts, without introducing new axioms. Major features of HOLCF '11 include two high-level definition packages: the Fixrec package for defining recursive functions, and the Domain package for defining recursive datatypes. Each of these uses the domain-theoretic concept of least fixed points to translate user-supplied recursive specifications into safe low-level definitions. Together, these tools make it easy for users to translate a wide variety of functional programs into the formalism of HOLCF. Theorems generated by the tools also make it easy for users to reason about their programs, with a very high level of confidence in the soundness of the results. As a case study, we present a fully mechanized verification of a model of concurrency based on powerdomains. The formalization depends on many features unique to HOLCF '11, and is the first verification of such a model in a formal proof tool.

Functional programming (FP) has progressively become more prevalent and techniques from the FP paradigm has been implemented in many different Imperative object-oriented programming (OOP) languages. However, there is no indication that OOP is going out of style. Nevertheless the increased popularity in FP has sparked new discussions across the Internet between the FP and OOP communities regarding a multitude of related aspects. These discussions could provide insights into the questions and challenges faced by programmers today. This thesis investigates these online discussions in a small and contemporary scale in order to identify the most discussed aspect of FP and OOP. Once identified the statements and claims made by various discussion participants were selected and compared to literature relating to the aspects and the theory behind the paradigms in order to determine whether there was any discrepancies between practitioners and theory. It was done in order to investigate whether the practitioners had different ideas in the form of best practices that could influence theories. The most discussed aspect within FP and OOP was ​immutability and state​ relating primarily to the aspects of ​concurrency ​ and ​performance​ . This thesis presents a selection of representative quotes that illustrate the different points of view held by groups in the community and then addresses those claims by investigating what is said in literature. It was shown that there were no direct discrepancies between the practitioners and the theory.

Com o avanço tecnológico dos últimos anos passou a ser normal vermos microprocessadores com múltiplos núcleos (cores). A expectativa é de que o crescimento da quantidade de núcleos passe a ser maior do que o crescimento da velocidade desses núcleos. Assim, além de se preocuparem em otimizar algoritmos sequenciais, os programadores começaram a dar mais atenção às possibilidades de aproveitamento de toda a capacidade oferecida pelos diversos cores. Existem alguns modelos de programação que permitem uma abordagem concorrente. O modelo de programação concorrente mais adotado atualmente é o baseado em threads, que utiliza memória compartilhada e é adotado em Java. Um outro modelo é o baseado em troca de mensagens, no qual as entidades computacionais ativas são denominadas atores. Nesse trabalho, estudamos a linguagem Scala e seu modelo de atores. Além disso, implementamos em Scala uma versão paralela de um algoritmo de classicação que simula o sistema imunológico dos animais, o AIRS paralelo, e comparamos seu desempenho com a versão em Java. / With the technological advance of the last years it has been normal to see microprocessors with multiple cores. The expectation is that the growth of number of cores becomes greater than the growth of the speed of these cores. This way, besides worrying about optimizing sequential algorithms, developers started to give more attention to the possibilities of proting from all capacity offered by the cores. There exists a few programming models that allow a concurrent approach. In these days, the most adopted concurrent programming model is the one based on threads, which uses shared memory and is adopted in Java. Other model is based on message passing, on which the active computational entities are called actors. In this project, we studied Scala language and its model based on actors. Besides that, we implemented in Scala a parallel version of a classification algorithm that simules the immune system of the animals, parallel AIRS, and compared its performance with the Java version.

This paper main goal is to introduce the basic language and programming styles of the mathematical software Mathematica (5.2), and applies it to solve problems in algebra, calculus, linear algebra, probability and statistics. We hope readers can enhance the interest of learning mathematics by the aid of software, verify the common theorem using the software, and solving mathematical problems.

The intricate concepts of ad-hoc polymorphism and overloading permeate the field of programming languages despite their somewhat nebulous definitions. With the perspective afforded by the state of the art, object-oriented Fortress programming language, this thesis presents a contemporary account of ad-hoc polymorphism and overloading in theory and in practice. Common language constructs are reinterpreted with a new emphasis on overloading as a key facility. Furthermore, concrete problems with overloading in Fortress, encountered during the author's experience in the development of the language, are presented with an emphasis on the ad hoc nature of their solutions. / text

In Artificial Intelligence, especially in area of constraint programming, it's popular to design various modeling languages which allow solving problems on domain level and by using domain specific abstractions. Techniques known from research on Domain-Specific Languages are often useful in this effort. Functional programming languages offer new tools for designing such languages, particularly Domain-Specific Embedded Languages. This work investigates the advantages and disadvantages of using functional programming for designing and implementing a Domain-Specific Embedded Language for state space search problems.

S'assurer qu'un programme informatique se comporte bien, surtout dans des applications critiques (santé, transport, énergie, communications, etc.) est de plus en plus important car les ordinateurs et programmes informatiques sont de plus en plus omniprésents, voir essentiel au bon fonctionnement de la société. Mais comment vérifier qu'un programme se comporte comme prévu, quand les informations qu'il prend en entrée sont de très grande taille, voire de taille non bornée a priori ? Pour exprimer avec exactitude ce qu'est le comportement d'un programme, il est d'abord nécessaire d'utiliser un langage logique formel. Cependant, comme l'a montré Gödel dans, dans tout système formel suffisamment riche pour faire de l'arithmétique, il y a des formules valides qui ne peuvent pas être prouvées. Donc il n'y a pas de programme qui puisse décider si toute propriété est vraie ou fausse. Cependant, il est possible d'écrire un programme qui puisse vérifier la correction d'une preuve. Ce travail utilisera justement un tel programme, Coq, pour formellement vérifier la correction d'un certain programme. Dans cette thèse, nous expliquons le développement d'une nouvelle version de Rainbow, plus rapide et plus sûre, basée sur le mécanisme d'extraction de Coq. La version précédente de Rainbow vérifiait un certificat en deux étapes. Premièrement, elle utilisait un programme OCaml non certifié pour traduire un fichier CPF en un script Coq, en utilisant la bibliothèque Coq sur la théorie de la réécriture et la terminaison appelée CoLoR. Deuxièmement, elle appelait Coq pour vérifier la correction du script ainsi généré. Cette approche est intéressante car elle fournit un moyen de réutiliser dans Coq des preuves de terminaison générée par des outils extérieurs à Coq. C'est également l'approche suivie par CiME3. Mais cette approche a aussi plusieurs désavantages. Premièrement, comme dans Coq les fonctions sont interprétées, les calculs sont beaucoup plus lents qu'avec un langage où les programmes sont compilés vers du code binaire exécutable. Deuxièmement, la traduction de CPF dans Coq peut être erronée et conduire au rejet de certificats valides ou à l'acceptation de certificats invalides. Pour résoudre ce deuxième problème, il est nécessaire de définir et prouver formellement la correction de la fonction vérifiant si un certificat est valide ou non. Et pour résoudre le premier problème, il est nécessaire de compiler cette fonction vers du code binaire exécutable. Cette thèse montre comment résoudre ces deux problèmes en utilisant l'assistant à la preuve Coq et son mécanisme d'extraction vers le langage de programmation OCaml. En effet, les structures de données et fonctions définies dans Coq peuvent être traduits dans OCaml et compilées en code binaire exécutable par le compilateur OCaml. Une approche similaire est suivie par CeTA en utilisant l'assistant à la preuve Isabelle et le langage Haskell. / Making sure that a computer program behaves as expected, especially in critical applications (health, transport, energy, communications, etc.), is more and more important, all the more so since computer programs become more and more ubiquitous and essential to the functioning of modern societies. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite? In this work, we explain the development of a new, faster and formally proved version of Rainbow based on the extraction mechanism of Coq. The previous version of Rainbow verified a CPF le in two steps. First, it used a non-certified OCaml program to translate a CPF file into a Coq script, using the Coq libraries on rewriting theory and termination CoLoR and Coccinelle. Second, it called Coq to check the correctness of the script. This approach is interesting for it provides a way to reuse in Coq termination proofs generated by external tools. This is also the approach followed by CiME3. However, it suffers from a number of deficiencies. First, because in Coq functions are interpreted, computation is much slower than with programs written in a standard programming language and compiled into binary code. Second, because the translation from CPF to Coq is not certified, it may contain errors and either lead to the rejection of valid certificates, or to the acceptance of wrong certificates. To solve the latter problem, one needs to define and formally prove the correctness of a function checking whether a certificate is valid or not. To solve the former problem, one needs to compile this function to binary code. The present work shows how to solve these two problems by using the proof assistant Coq and its extraction mechanism to the programming language OCaml. Indeed, data structures and functions de fined in Coq can be translated to OCaml and then compiled to binary code by using the OCaml compiler. A similar approach was first initiated in CeTA using the Isabelle proof assistant.

Gameplay programming is vital for video game development and benefits from good tools and techniques. However, techniques are still used in the industry that involves describing how the computer operates. Reactive programming is a way to describe eventful and stateful computer programs declaratively, focusing on what the program should accomplish. This thesis uses the reactive library UniRx with the game engine Unity 5 to create an FPS with reactive techniques, and discusses the advantages and disadvantages of these. Object-oriented reactive programming is used to combine reactive objects with Unity’s component-based framework without using wrappers for non-reactive objects. The results include static methods for observable user input, patterns when defining game components with reactive content, and communication between game objects through interface components. It can be concluded that reactive programming for game programming enables the programmer to describe and understand game logic in a declarative manner. However, combining UniRx and Unity 5 led to complex patterns. Suggestion for future work is using reactive programming with game engines that allows to design game objects that are fully reactive. / Gameplay-programmering är avgörande för utveckling av videospel och har nytta av bra verktyg och tekniker. Dock används tekniker i spelbranschen som kräver att programmeraren beskriver hur datorn utför uppgifter. Reaktiv programmering är ett sätt att beskriva händelserika och föränderliga datorprogram med fokus på vad programmet ska utföra. Denna avhandling använder det reaktiva biblioteket UniRx med spelmotorn Unity 5 för att skapa en FPS med reaktiva tekniker, samt diskuterar fördelarna och nackdelarna med dessa. Objektorienterad reaktiv programmering används för att kombinera reaktiva objekt med Unity’s komponentbaserade ramverk utan att använda wrappers för icke-reaktiva objekt. Resultaten inkluderar statiska metoder för observerbar användarinput, programmeringsmönster för definition av spelkomponenter med reaktivt innehåll och kommunikation mellan spelobjekt via gränssnittskomponenter. Man kan dra slutsatsen att reaktiv programmering för spelprogrammering gör det möjligt för programmeraren att beskriva och förstå spellogik på ett deklarativt sätt. Kombinationen av UniRx och Unity 5 ledde emellertid till komplexa mönster. Förslag till framtida arbete är att använda reaktiv programmering med spelmotorer som gör det möjligt att designa spelobjekt som är helt reaktiva.