331 |
The Basic Scheme for the Evaluation of Functional Logic ProgramsPeters, Arthur 01 January 2012 (has links)
Functional logic languages provide a powerful programming paradigm combining the features of functional languages and logic languages. However, current implementations of functional logic languages are complex, slow, or both. This thesis presents a scheme, called the Basic Scheme, for compiling and executing functional logic languages based on non-deterministic graph rewriting. This thesis also describes the implementation and optimization of a prototype of the Basic Scheme. The prototype is simple and performs well compared to other current implementations.
|
332 |
A TRANSLATION OF OCAML GADTS INTO COQPedro da Costa Abreu Junior (18422613) 23 April 2024 (has links)
<p dir="ltr">Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. When that language is sufficiently similar to that of the proof assistant, one solution is to use a <i>shallow embedding</i> to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present <i>GSet</i>, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the translation algorithm between GADTml and gCIC, together with a proof of the soundness of this translation. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.</p>
|
333 |
Avoiding data inconsistency problems in the conceptual design of data bases: a semantic approachLeasure, David Elden. January 1984 (has links)
Call number: LD2668 .T4 1984 L42 / Master of Science
|
334 |
A language to support verification of embedded softwareSwart, Riaan 04 1900 (has links)
Thesis (MSc)--University of Stellenbosch, 2004. / ENGLISH ABSTRACT: Embedded computer systems form part of larger systems such as aircraft or chemical processing
facilities. Although testing and debugging of such systems are difficult, reliability is often
essential. Development of embedded software can be simplified by an environment that limits
opportunities for making errors and provides facilities for detection of errors. We implemented
a language and compiler that can serve as basis for such an experimental environment. Both
are designed to make verification of implementations feasible.
Correctness and safety were given highest priority, but without sacrificing efficiency wherever
possible. The language is concurrent and includes measures for protecting the address spaces
of concurrently running processes. This eliminates the need for expensive run-time memory
protection and will benefit resource-strapped embedded systems. The target hardware is
assumed to provide no special support for concurrency. The language is designed to be
small, simple and intuitive, and to promote compile-time detection of errors. Facilities for
abstraction, such as modules and abstract data types support implementation and testing of
bigger systems.
We have opted for model checking as verification technique, so our implementation language
is similar in design to a modelling language for a widely used model checker. Because of
this, the implementation code can be used as input for a model checker. However, since the
compiler can still contain errors, there might be discrepancies between the implementation
code written in our language and the executable code produced by the compiler. Therefore
we are attempting to make verification of executable code feasible. To achieve this, our
compiler generates code in a special format, comprising a transition system of uninterruptible
actions. The actions limit the scheduling points present in processes and reduce the different
interleavings of process code possible in a concurrent system. Requirements that conventional
hardware places on this form of code are discussed, as well as how the format influences
efficiency and responsiveness. / AFRIKAANSE OPSOMMING: Ingebedde rekenaarstelsels maak deel uit van groter stelsels soos vliegtuie of chemiese prosesseerfasiliteite.
Hoewel toetsing en ontfouting van sulke stelsels moeilik is, is betroubaarheid
dikwels onontbeerlik. Ontwikkeling van ingebedde sagteware kan makliker gemaak word met
'n ontwikkelingsomgewing wat geleenthede vir foutmaak beperk en fasiliteite vir foutbespeuring
verskaf. Ons het 'n programmeertaal en vertaler geïmplementeer wat as basis kan dien vir
so 'n eksperimentele omgewing. Beide is ontwerp om verifikasie van implementasies haalbaar
te maak.
Korrektheid en veiligheid het die hoogste prioriteit geniet, maar sonder om effektiwiteit prys
te gee, waar moontlik. Die taal is gelyklopend en bevat maatreëls om die adresruimtes van
gelyklopende prosesse te beskerm. Dit maak duur looptyd-geheuebeskerming onnodig, tot
voordeel van ingebedde stelsels met 'n tekort aan hulpbronne. Daar word aangeneem dat
die teikenhardeware geen spesiale ondersteuning vir gelyklopendheid bevat nie. Die programmeertaal
is ontwerp om klein, eenvoudig en intuïtief te wees, en om vertaaltyd-opsporing van
foute te bevorder. Fasiliteite vir abstraksie, byvoorbeeld modules en abstrakte datatipes,
ondersteun implementering en toetsing van groter stelsels.
Ons het modeltoetsing as verifikasietegniek gekies, dus is die ontwerp van ons programmeertaal
soortgelyk aan dié van 'n modelleertaal vir 'n modeltoetser wat algemeen gebruik word.
As gevolg hiervan kan die implementasiekode as toevoer vir 'n modeltoetser gebruik word.
Omdat die vertaler egter steeds foute kan bevat, mag daar teenstrydighede bestaan tussen die
implementasie geskryf in ons implementasietaal, en die uitvoerbare masjienkode wat deur die
vertaler gelewer word. Daarom poog ons om verifikasie van die uitvoerbare masjienkode haalbaar
te maak. Om hierdie doelwit te bereik, is ons vertaler ontwerp om 'n spesiale formaat
masjienkode te genereer bestaande uit 'n oorgangstelsel wat ononderbreekbare (atomiese) aksies
bevat. Die aksies beperk die skeduleerpunte in prosesse en verminder sodoende die aantal
interpaginasies van proseskode wat moontlik is in 'n gelyklopende stelsel. Die vereistes wat
konvensionele hardeware aan dié spesifieke formaat kode stel, word bespreek, asook hoe die formaat effektiwiteit en reageerbaarheid van die stelsel beïnvloed.
|
335 |
Integrating programming languages and databases via program analysis and language designWiedermann, Benjamin Alan 23 August 2010 (has links)
Researchers and practitioners alike have long sought to integrate programming
languages and databases. Today's integration solutions focus on the data-types of
the two domains, but today's programs lack transparency. A
transparently persistent program operates over all objects
in a uniform manner, regardless of whether those objects reside in memory or in a
database. Transparency increases modularity and lowers the barrier of adoption in
industry. Unfortunately, fully transparent programs perform so poorly that no one
writes them. The goal of this dissertation is to increase the performance of
these programs to make transparent persistence a viable programming paradigm.
This dissertation contributes two novel techniques that integrate programming
languages and databases. Our first contribution--called query
extraction--is based purely on program analysis. Query extraction analyzes a
transparent, object-oriented program that retrieves and filters collections of
objects. Some of these objects may be persistent, in which case the program
contains implicit queries of persistent data. Our interprocedural program
analysis extracts these queries from the program, translates them to explicit
queries, and transforms the transparent program into an equivalent one that
contains the explicit queries. Query extraction enables programmers to write
programs in a familiar, modular style and to rely on the compiler to transform
their program into one that performs well.
Our second contribution--called RBI-DB+--is an extension
of a new programming language construct called a batch block. A batch
block provides a syntactic barrier around transparent code. It also provides a
latency guarantee: If the batch block compiles, then the code that appears in it
requires only one client-server communication trip. Researchers previously have
proposed batch blocks for databases. However, batch blocks cannot be modularized
or composed, and database batch blocks do not permit programmers to modify
persistent data. We extend database batch blocks to address these concerns and
formalize the results.
Today's technologies integrate the data-types of programming languages and
databases, but they discourage programmers from using procedural abstraction.
Our contributions restore procedural abstraction's use in enterprise
applications, without sacrificing performance. We argue that industry should
combine our contributions with data-type integration. The result would be a
robust, practical integration of programming languages and databases. / text
|
336 |
Modèles Formels pour la Programmation et la Composition de Systèmes Distribués CorrectsHenrio, Ludovic 19 July 2012 (has links) (PDF)
Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.
|
337 |
Normalisation by evaluation in the compilation of typed functional programming languagesLindley, Sam January 2005 (has links)
This thesis presents a critical analysis of normalisation by evaluation as a technique for speeding up compilation of typed functional programming languages. Our investigation focuses on the SML.NET compiler and its typed intermediate language MIL. We implement and measure the performance of normalisation by evaluation for MIL across a range of benchmarks. Taking a different approach, we also implement and measure the performance of a graph-based shrinking reductions algorithm for SML.NET. MIL is based on Moggi’s computational metalanguage. As a stepping stone to normalisation by evaluation, we investigate strong normalisation of the computational metalanguage by introducing an extension of Girard-Tait reducibility. Inspired by previous work on local state and parametric polymorphism, we define reducibility for continuations and more generally reducibility for frame stacks. First we prove strong normalistion for the computational metalanguage. Then we extend that proof to include features of MIL such as sums and exceptions. Taking an incremental approach, we construct a collection of increasingly sophisticated normalisation by evaluation algorithms, culminating in a range of normalisation algorithms for MIL. Congruence rules and alpha-rules are captured by a compositional parameterised semantics. Defunctionalisation is used to eliminate eta-rules. Normalisation by evaluation for the computational metalanguage is introduced using a monadic semantics. Variants in which the monadic effects are made explicit, using either state or control operators, are also considered. Previous implementations of normalisation by evaluation with sums have relied on continuation-passing-syle or control operators. We present a new algorithm which instead uses a single reference cell and a zipper structure. This suggests a possible alternative way of implementing Filinski’s monadic reflection operations. In order to obtain benchmark results without having to take into account all of the features of MIL, we implement two different techniques for eliding language constructs. The first is not semantics-preserving, but is effective for assessing the efficiency of normalisation by evaluation algorithms. The second is semantics-preserving, but less flexible. In common with many intermediate languages, but unlike the computational metalanguage, MIL requires all non-atomic values to be named. We use either control operators or state to ensure each non-atomic value is named. We assess our normalisation by evaluation algorithms by comparing them with a spectrum of progressively more optimised, rewriting-based normalisation algorithms. The SML.NET front-end is used to generate MIL code from ML programs, including the SML.NET compiler itself. Each algorithm is then applied to the generated MIL code. Normalisation by evaluation always performs faster than the most naıve algorithms— often by orders of magnitude. Some of the algorithms are slightly faster than normalisation by evaluation. Closer inspection reveals that these algorithms are in fact defunctionalised versions of normalisation by evaluation algorithms. Our normalisation by evaluation algorithms perform unrestricted inlining of functions. Unrestricted inlining can lead to a super-exponential blow-up in the size of target code with respect to the source. Furthermore, the worst-case complexity of compilation with unrestricted inlining is non-elementary in the size of the source code. SML.NET alleviates both problems by using a restricted form of normalisation based on Appel and Jim’s shrinking reductions. The original algorithm is quadratic in the worst case. Using a graph-based representation for terms we implement a compositional linear algorithm. This speeds up the time taken to perform shrinking reductions by up to a factor of fourteen, which leads to an improvement of up to forty percent in total compile time.
|
338 |
Design of an object-oriented language syntax for UIL, the User Interface Language of the Space Station FREEDOMSos, Garrett Tim, 1959- January 1989 (has links)
The design of a new computer language, called the User Interface Language (UIL), is analyzed and evaluated by coding a representative procedure. UIL will provide the man-machine interface for command procedures on the Space Station FREEDOM. The UIL procedure written is modeled after an operational procedure used in the Space Shuttle program. This work provides a concrete test case to verify that UIL can be used to implement procedures for the Space Station. The object oriented approach taken with UIL is based on the successful application of these concepts for a variety of other software tools in operation today. Three major enhancements are proposed in this thesis: event handlers, data structures, and class/object creation capabilities. The addition of these capabilities changes the character of UIL from an object manipulation language to an object based language. The new capabilities, if adopted, will profoundly change the future of UIL.
|
339 |
Javascript and Politics: How a Toy Language Took Over the WorldMcQueen, Sean 01 January 2013 (has links)
The most important programming languages are the ones that manage to capitalize on emerging frontiers in computing. Although JavaScript started its life as a toy language, the explosive growth of the web since 1995 and the invention of the web application have transformed the language’s syntax, potential and importance. JavaScript today is powerful and expressive. But is the language good enough to power the future of the web? How does the messy political past of JavaScript affect web development today, and how will it affect web development in the future?
The paper first examines the political history of JavaScript from its origins at Netscape through today. Then a case study of pure JavaScript web development using the NodeJS and AngularJS is presented and analyzed. Finally, several potential paths forward for the language are considered, including a discussion and analysis of Microsoft’s TypeScript, Mozilla’s ASM.js and Google’s Dart.
|
340 |
Transformacijų tarp konkrečių programavimo kalbų abstrakčios sintaksės medžių ir nuo kalbos nepriklausomų abstrakčios sintaksės medžių tyrimas / Investigation of transformations between abstract syntax trees of a concrete programming language and language-independent abstract syntax treesStankevičius, Rytis 13 August 2010 (has links)
Medžių tipo duomenų struktūras transformuojantys įrankiai naudojami išspręsti gausybę įvairaus tipo problemų: kompiliatorių, kodo optimizatorių, dokumentacijos ir kodo generavimo įrankių kūrimo ir pan. Bet nei vienas iš šių egzistuojančių įrankių nėra specialiai skirtas abstrakčios sintaksės medžių transformacijoms į nuo kalbos nepriklausomą formą, ar iš jo.
Šis magistro darbas aprašo sistemą, kuri pateiktą konkretų abstrakčios sintaksės medį (abstrakčios sintaksės medį, kuris išreiškia realios programavimo kalbos – C#, Java, Ruby ar pan. –
programinio kodo struktūrą) transformuoja į nuo kalbos nepriklausomą abstrakčios sintaksės medį, bei atvirkščiai. Taisyklės, aprašančios vieno medžio transformavimą į kitą, yra aprašytos XML formatu paremtuose failuose, kurių struktūra aiški ir paprasta. Sistemą galima naudoti kaip nepriklausomą komponentą arba kaip įrankį trečiųjų šalių programinėje įrangoje. Tiek sistemos pagrindinės bibliotekos, tiek jas naudojantys įrankiai yra parašyti Java programavimo kalba.
Sistemos tyrimu siekta įrodyti du dalykus: kad sistema gali teisingai transformuoti pateiktąjį konkretų abstrakčios sintaksės medį į jį atitinkantį bendrinį medį, ir atvirkščiai; ir kad transformavimo vykdymo laikas yra leistinose ribose. Abiejų tikslų buvo pasiekta. Remiantis šiais rezultatais prieita išvados, jog sistema yra tinkamas kandidatas tapti pagrindu trečiųjų šalių įrankiams, atliekantiems programinio kodo migravimą, pertvarkymus (angl. „refactoring“), modelių... [toliau žr. visą tekstą] / Tools for transforming tree-like data structures are used for solving a range of different problems, such as creation of compilers, code optimizers, documentation and code generation tools, etc. But none of these existing tools seem to be specialized in transforming abstract syntax trees to a language-independent format or from it. This master‘s thesis describes a system that takes concrete abstract syntax trees (ASTs that represent the structure of code written in a real programming language, such a C#, Java, Ruby, etc.) and transforms them into language-independent abstract syntax trees, and vice versa. Rules for mapping one AST to the other are defined in XML-based configuration files that have a simple and clear structure. The system can be used as a stand-alone tool or used as component in third party software. Both the system’s core libraries and tools are written in Java. The purpose of the system’s investigation was to prove two things: that the system can correctly transform a given specific AST to an equivalent generic AST, and vise versa; and that the transformation execution time is within an acceptable range. Both goals were met. This led to a conclusion that the system is a suitable candidate for use by third party tools that handle code migration, refactoring, model transformation and other types of similar tasks.
|
Page generated in 0.0373 seconds