FREE ELECTRONIC LIBRARY - Abstract, dissertation, book

Pages:   || 2 | 3 | 4 |

«Abstract. Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We show how ...»

-- [ Page 1 ] --

Animating the Formalised Semantics

of a Java-like Language

Andreas Lochbihler1 and Lukas Bulwahn2

Karlsruher Institut f¨r Technologie, andreas.lochbihler@kit.edu


Technische Universit¨t M¨nchen, bulwahn@in.tum.de

a u

Abstract. Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We

show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle’s code generation facilities, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell’s definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.

1 Introduction In the last few years, substantial work has been devoted to the techniques and tools for executing formal specifications from Isabelle/HOL, on the levels of both prover infrastructure [5,8,9] and formalisations of foundational notions and concepts [6,11,18]. But so far, applications (e.g. [4,19,20]) have been designed for executability and restricted to purely functional specifications. A benchmark to test whether the aforementioned techniques mix well and scale to large formalisations has been missing.

In this work, we study how to apply code generation techniques to the JinjaThreads project [15,16,17], which formalises a substantial subset of multithreaded Java source and bytecode. JinjaThreads constitutes a good benchmark for three reasons: (i) It is a large formalisation (70k lines of definitions and proofs) that involves a broad range of advanced Isabelle features. (ii) As a programming language, type system, and semantics, it has a built-in notion of execution. This sets the goal for what should be executable. (iii) It focuses on proofs and modularity rather than code generation, i.e. complications in specifications and proofs for the sake of direct code generation were out of the question. Hence, it tests if code generation works “in the wild” and not only for specialised developments.

Our main contribution here is to discuss what was needed to automatically generate a well-formedness checker and an interpreter for JinjaThreads programs from the Isabelle formalisation, and what the pitfalls were. Thereby, we demonstrate how to combine the different techniques and tools such that changes to the existing formalisation stay minimal. Our contributions fall into two parts.

On the system’s side, we enhanced Isabelle’s code generator for inductive predicates (§2.1) to obtain a mature tool for our needs. It now compiles inductive definitions and first-order predicates, interpreted as logic programs, to functional implementations. Furthermore, we present a practical method to overcome the poor integratability of Isabelle’s code generator into Isabelle’s module system (§2.2). Finally, we describe a tabled implementation of the reflexive transitive closure (§2.3) and an executable version of Russell’s definite description operator (§2.4), which are now part of the Isabelle/HOL library.

On JinjaThreads’ side, we animated the formalisation (see §3.1 for an overview) through code generation: Many of its inductive definitions, we had to refine for compilation or, if this was impossible, implement manually (§3.2 and §3.3).

To obtain execution traces of JinjaThreads programs, we adapted the state representation and formalised two schedulers (§3.4). In §3.5, we explain how to add memoisation to avoid frequently recomputing common functions, e.g. lookup functions, without polluting the existing formalisation. Clearly, as the generated code naively interprets source code programs, we cannot expect it to be as efficient as an optimising Java virutal machine (JVM). Nevertheless, we evaluated the performance of the generated interpreter (§3.6). Simple optimisations that we describe there speed up the interpreter by three orders of magnitude. Hence, it is sufficiently efficient to handle Java programs of a few hundred lines of code.

We conclude our contributions by distilling our experience into a few guidelines on how to develop formalisations to be executable ones. Rather than imposing drastic changes on the formalisation, they pinpoint common pitfalls. §4 explains why and how to avoid them.

The interpreter and the full formalisation is available online in the Archive of Formal Proofs [17]. To make the vast supply of Java programs available for experimenting and testing with the semantics, we have written the (unverified) conversion tool Java2Jinja as a plug-in to the Eclipse IDE. It converts Java class declarations into JinjaThreads


syntax. The latest development version is available at http://pp.info.uni-karlsruhe.de/git/Java2Jinja/.

1.1 Related work Code generation (of functional implementations) from Isabelle/HOL is a wellestablished business. Mari´ [19] presents a formally verified implementation of c a SAT solver. In the CeTA project, Thiemann and Sternagel [20] generate a self-contained executable termination checker for term rewriting systems. The Flyspeck project uses code generation to compute the set of tame graphs [4]. All these formalisations were developed with executability in mind. Complications in proofs to obtain an efficiently executable implementation were willingly taken and handling them are large contributions of these projects.

Code generation in Coq [13] has been used in various developments, notably the CompCert compiler [12] and the certificate checkers in the MOBIUS project [3]. Like in Isabelle, functional specifications pose no intrinsic problems.

Although code extraction is in principle possible for any Coq specification, mathematical theories can lead to “a nightmare in term of extracted code efficiency and readability” [13]. Hence, Coq’s users, too, are facing the problem of how to extract (roughly) efficient code from specifications not aimed towards executability. ACL2 and PVS translate only functional implementations to Common Lisp.

In [5], we have reported on generating code from non-functional specifications. Recently, Nipkow applied code generation for inductive predicates to animate the semantics and various program analyses of an educational imperative language (personal communication). All these applications were tiny formalisations compared to JinjaThreads.

Some formalisations of the JVM in theorem provers are directly executable.

The most complete is the M6 model of a JVM by Lui and Moore [14] in ACL2, which covers the CLDC specification. Farzan et al. [7] report on a JVM formalisation in Maude’s rewriting logic. ACL2’s and Maude’s logics are directly executable, i.e., they force the user to write only executable formalisations. While JinjaThreads studies meta-language properties like type safety for a unified model of Java and Java bytecode, these JVM formalisations aim at verifying properties of individual programs. Atkey [1] presents an executable JVM model in Coq. He concentrates on encoding defensive type checks as dependent types, but does not provide any data on the efficiency.

1.2 Background: the Code Generator Framework and Refinement Isabelle’s code generator [9] turns a set of equational theorems into a functional program with the same equational rewrite system. As it builds on equational logic, the translation guarantees partial correctness by construction and the user may easily refine programs and data without affecting her formalisation globally.

Program refinement can separate code generation issues from the rest of the formalisation. As any (executable) equational theorem suffices for code generation, the user may locally derive new (code) equations to use upon code generation.

Hence, existing definitions and proofs remain unaffected, which has been crucial for JinjaThreads.

For data refinement, the user may replace constructors of a datatype by other constants and derive equations that pattern-match on these new (pseudo-)constructors. Neither need the new constructors be injective and pairwise disjoint, nor exhaust the type. Again, this is local as it affects only code generation, but not the logical properties of the refined type. Conversely, one cannot exploit the type’s new structure inside the logic. Only type constructors can be refined;

some special types (such as a ⇒ b option for maps) must first be wrapped in an (isomorphic) type of their own (e.g. ( a, b) mapping).

Isabelle’s standard library defines such special-purpose types for sets and maps with standard operations. Associative lists and red-black trees implement them via data refinement. FinFuns [18] are almost-everywhere constant functions; they provide an executable universal quantifier thanks to data refinement to associative lists. The Isabelle Collections Framework (ICF) [11] advocates dealing with refinement in the logic instead of hiding it in the code generator. Locales, i.e. Isabelle modules, specify the abstract operations, concrete implementations interpret them. This allows for executing truly underspecified functions.

2 Code Generation in Isabelle In this section, we present our contributions that JinjaThreads has motivated, but that are generally applicable. Consequently, they have been integrated into Isabelle’s main system and library. First, we present the code generator for inductive predicates and our improvements to it (§2.1). Then, we describe our approach to overcome the problematic situation with code generation and locales (§2.2). Finally, we sketch formalisations for enhanced implementations for the reflexive transitive closure (§2.3) and the definite description operator (§2.4), which are employed in JinjaThreads’ type system, for example.

2.1 The Predicate Compiler The predicate compiler [5] translates specifications of inductive predicates, i.e. the introduction rules, into executable equational theorems for Isabelle’s code generator. The translation is based on the notion of modes. A mode partitions the arguments into input and output. For a given predicate, the predicate compiler infers the set of possible modes such that all terms are ground during execution.

Lazy sequences handle the non-determinism of inductive predicates. By default, the equations implement a Prolog-style depth-first execution strategy. Since its

initial description [5], we improved the predicate compiler in four aspects:

First, mode annotations restrict the generation of code equations to modes of interest. This is necessary because the set of modes is exponential in the number of arguments of a predicate. Therefore, the space and time consumption of the underlying mode inference algorithm grows exponentially in that number; for all applications prior to JinjaThreads, this has never posed a problem. In case of many arguments (up to 15 in JinjaThreads), the plain construction of this set of modes burns up any available hardware resource. To sidestep this limitation, modes can now be declared and hence they are not inferred, but only checked to be consistent.

Second, we also improved the compilation scheme: The previous one sequentially checked which of the introduction rules were applicable. Hence, the input values were repeatedly compared to the terms in the conclusion of each introduction rule by pattern matching. For large specifications, such as JinjaThreads’ semantics (contains 88 rules), this naive compilation made execution virtually impossible due to the large number of rules. To obtain an efficient code expression, we modified the compilation scheme to partition the rules by patterns of the input values first and then only compose the matching rules – this resembles similar techniques in Prolog compilers, such as clause indexing and switch detection.

We report on the performance improvements due to this modification in §3.6.

Third, the predicate compiler now offers non-intrusive program refinement, i.e., the user can declare alternative introduction rules. For an example, see §3.3.

Fourth, the predicate compiler was originally limited to the restricted syntactic form of introduction rules. We added some preprocessing that transforms definitions in predicate logic to a set of introduction rules. Type-safe method overriding (§3.2) gives an example.

2.2 Isabelle Locales and Code Generation Locales [2] in Isabelle allow parametrised theory and proof development. In other words, locales allow to prove theorems abstractly, relative to a set of fixed parameters and assumptions. Interpretation of locales transfers theorems from their abstract context to other (concrete) contexts by instantiating the parameters and proving the assumptions. JinjaThreads uses locales to abstract over different memory consistency models (§3.3) and schedulers (§3.4), and to underspecify operations on abstract data structures.

As code generation requires equational theorems in the (foundational) theory context, theorems that reside in the context of a locale cannot serve as code equations directly, but must be transferred into the theory context. For example, consider a locale L with one parameter p, one assumption A p and one definition f =... that depends on p. Let g be a function in the theory context for which A (g z) holds for all z. We want to generate code for f where p is instantiated to g z.

The Isabelle code generator tutorial proposes interpretation and definition:

One instantiates p by g z and discharges the assumption with A (g z), for arbitrary z. This yields the code equation f (g z) =... which is ill-formed because the left-hand side applies f to the non-constructor constant g. For code generation, one must manually define a new function f’ by f’ z = f (g z) and derive f’ z =... as code equation. This approach is unsatisfactory for two reasons: It requires to manually re-define all dependent locale definitions in the theory context (and for each interpretation), and the interpretation must be unconditional, i.e., A (g z) must hold for all z. In JinjaThreads, the latter is often violated, e.g. g z satisfies A only if z is well-formed.

Pages:   || 2 | 3 | 4 |

Similar works:

«Machine Learning: The High-Interest Credit Card of Technical Debt D. Sculley, Gary Holt, Daniel Golovin, Eugene Davydov, Todd Phillips, Dietmar Ebner, Vinay Chaudhary, Michael Young {dsculley,gholt,dgg,edavydov}@google.com {toddphillips,ebner,vchaudhary,mwyoung}@google.com Google, Inc Abstract Machine learning offers a fantastically powerful toolkit for building complex systems quickly. This paper argues that it is dangerous to think of these quick wins as coming for free. Using the framework...»

«0 SUMMIT FOR ADDRESSING DISPROPORTIONALITY PLANNING COMMITTEE The Summit for Addressing Disproportionality is one component of The Disproportionality Technical Assistance Network (DTAN). This event has been known as the Annual Disproportionality Conference (2005-2008), the CREATE a Culturally Responsive Environment Conference (2009), and the CREATE Conference (2010-2013). During 2013, the CREATE grant initiative underwent reconfiguration efforts reflecting the sustainability of the purpose,...»

«The Wells Fargo Rewards® Program Terms and Conditions Effective: September 2013 Section 1: Your Contract With Us Section 2: Your Rewards Program Account, Rewards Currency And Earning Mechanisms Section 3: Options For Redeeming Rewards Section 4: Transfer And Gifting Of Rewards Currency Section 5: About Rewards Redemption Section 6: Dispute Resolution Program: Arbitration Provision Section 1: Your Contract With Us “You”, “Your”, or “Customer” means, as applicable, each person who is...»

«Balázs Tôkey* Insurance Contracts in the New Hungarian Civil Code I Introduction We would like to give a short overview of the regulation of insurance contracts in the new Hungarian Civil Code (Act V of 2013 on the Civil Code, hereinafter referred to as NHCC)1 in this paper. Of course, we cannot interpret this topic in detail in a short paper and so we will just focus on the following fundamental questions: – What are the characteristics of insurance contracts according to the NHCC? Which...»

«44 Электронное научное издание «Международный электронный журнал. Устойчивое развитие: наука и практика» вып. 2 (3), 2009, ст. 3. www.yrazvitie.ru ББК К01, УДК 627.09 АНАЛИЗ СЦЕНАРИЕВ РАЗВИТИЯ КАЗАХСТАНА В УСЛОВИЯХ МИРОВОГО КРИЗИСА Искаков Нурлан Абдильдаевич, доктор экономических наук,...»

«Zur Einrichtung von Nationalparks in Syrien – Exemplarisch untersucht am Tal des Al Asi/Orontes vorgelegt von Dip.–Ing. Sabah AlBrahim aus Hama, Syrien von der Fakultät VI Planen Bauen Umweltder Technischen Universität Berlin zur Erlangung des akademischen Grades Doktorin der Ingenieurwissenschaften -Dr.Ing.genehmigte Dissertation Promotionsausschuss: Vorsitzende: Prof. Dr. Cordula Loidl-Reisch Gutachter: Prof. Dr. Johannes Küchler Gutachterin: Prof. Dr. Sonja Nebel Gutachter: Prof. Dr....»

«Earth & E-nvironment 3:115-158 University of Leeds Press The Effects of Varied Management Techniques on the Recreation of Lowland Heathland Habitats in Devon Katie S. Fortnam School of Earth & Environment, University of Leeds, Leeds, W. Yorkshire LS2 9JT; Tel: 0113 3436461 Abstract Lowland heathland habitats have decreased extensively in recent years, making it a priority habitat for conservation. Governmental targets have now been set to create, restore and expand heathland in the UK. For...»

«СЭМ РУЖАНСКИЙ Разговоры по душам Избранные интервью Сэм Ружанский разговоры по душам Избранные интервью Бостон • 2013 • boston Cэм Ружанский Разговоры по душам. Избранные интервью Печатается в авторской редакции Sam Ruzhansky Intimate Conversations. Selected Interviews (Razgovory po dusham. Izbrannye intervyu) Copyright ©...»

«TECHNISCHE UNIVERSITÄT MÜNCHEN Lehrstuhl für Entwicklungsgenetik Nedd8 in the brain Its impact on synaptic function and the role of PSD-95 Marisa Brockmann Vollständiger Abdruck der von der Fakultät Wissenschaftszentrum Weihenstephan für Ernährung, Landnutzung und Umwelt der Technischen Universität München zur Erlangung des akademischen Grades eines Doktors der Naturwissenschaften genehmigten Dissertation. Vorsitzender: Univ.-Prof. Dr. E. Grill Prüfer der Dissertation: 1. Univ.-Prof....»

«Easy Download Vampireville Vampire Kisses 3 By Ellen Schreiber in here. Also read document Vampireville Vampire Kisses 3 By Ellen Schreiber online VAMPIREVILLE VAMPIRE KISSES 3 BY ELLEN SCHREIBER PDF Manual guide vampireville vampire kisses 3 by ellen schreiber PDF update. So you are person who likes to download vampireville vampire kisses 3 by ellen schreiber Pdf to any kind of device,whether its your laptop, Kindle or iPhone, there are more options now than ever before. Perhaps because of the...»

«Frank Schönefeld Praxisleitfaden Enterprise 2.0 Wettbewerbsfähig durch neue Formen der Zusammenarbeit, Kundenbindung und Innovation Basiswissen zum erfolgreichen Einsatz von Web 2.0-Technologien Inhalt 1 Das Enterprise 2.0 im digitalen Lebensund Geschäftsraum 1.1 Die Herausbildung des digitalen Lebensund Geschäftsraumes 1.2 Die Feinstruktur des digitalen Lebensund Geschäftsraums. 3 1.3 Phasen und Wirkungsradien in der Entwicklung des Internets 1.3.1 Das technische Internet 1.3.2 Das Web...»

«418 Michel Lallement, Olivier Mériaux: Status and Contracts in Industrial Relations Michel Lallement, Olivier Mériaux* Status and Contracts in Industrial Relations. „La Refondation sociale”, a new Bottle for an old (French) Wine? ** Since 1999, the main French employers’ organisation (Medef) has been promoting a radical transformation of the institutional framework of industrial relations and the welfare state. This initiative, known as the „Social Re-foundation” agenda, has started to...»

<<  HOME   |    CONTACTS
2016 www.abstract.xlibx.info - Free e-library - Abstract, dissertation, book

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.