1. Shin-Chen Mu (Academia Sinica, Taiwan)
An Algebraic Approach to Bi-directional Updating
In many occasions would one encounter the task of maintaining the consistency of two pieces of structured data that are related by some transform --- synchronising bookmarks in different web browsers, the source and the view in an editor, or views in databases, to name a few. This paper proposes a formal model of such tasks, basing on a programming language allowing injective functions only. The programmer designs the transformation as if she is writing a functional program, while the synchronisation behaviour is automatically derived by algebraic reasoning. The main advantage is being able to deal with duplication and structural changes. The result was be integrated to our structure XML editor in the Programmable Structured Document project.
1. Robert Glück (University of Copenhagen)
Reversible Machine Code and Its Abstract Processor Architecture
The talk explain the concept and programming of an abstract register machine with local on-the fly program inversion. We exemplify its use with a reversible integer FFT program. Joint work with Tetsuo Yokoyama and Holger Bock Axelsen.
1. Dana N. Xu (University of Cambridge)
Static Contract Checking for Haskell
Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification tool for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.
2. Kazutaka Matsuda (University of Tokyo)
Type Specialization for Effective Bidirectionalization
A bidirectional transformation is a pair of transformations, a forward transformation and a backward transformation, where a forward transformation maps one data structure called source to another called view, and a corresponding backward transformation reflects changes on the view to the source. Its practical applications include replicated data synchronization, presentation-oriented editor development, tracing software development, and document format conversion.
It is, however, difficult to develop bidirectional transformations, because the forward and backward mappings must satisfy the bidirectional properties for consistency. It is even more difficult if we want to obtain ``better'' bidirectional transformations with, for example, clearer consistent semantics between sources and views and more updates on views. To resolve this problem, a program transformation named bidirectionalization is proposed, in which a useful backward transformation can be derived automatically from a given forward transformation based on derivation of a complementary function. However, the language there for describing forward transformations is still too restrictive to write many practical transformations.
In this presentation, we relax the restrictions on the previous language by supporting forest concatenation and look-ahead mechanism specified by regular expression types, which allows us to write practical transformations. In the language, a program transformation named type specialization not only enables us to obtain ``better'' backward transformations but also provides exact type checking of transformations.
1. João Saraiva (Universidade do Minho)
Strictification of Circular Lazy Programs
In this talk we present techniques to model circular lazy programs in a strict, purely functional setting. Circular lazy programs model any algorithm based on multiple traversals over a recursive data structure as a single traversal function. Such elegant and concise circular programs are defined in a (strict or lazy) functional language and they are transformed into efficient strict and deforested, multiple traversal programs by using well-known attribute grammars-based techniques. We will also present a Haskell-based tool that implements this transformation. The first benchmarks of the different implementations will be discussed.
2. João Paulo Fernandes (Universidade do Minho)
A shortcut fusion rule for circular program calculation
In this talk, we present a shortcut deforestation technique to calculate circular programs. The technique we propose takes as input the composition of two functions, such that the first builds an intermediate structure and some additional context information which are then processed by the second one, to produce the final result. Our transformation into circular programs achieves intermediate structure deforestation and multiple traversal elimination. Furthermore, the calculated programs preserve the termination properties of the original ones.
Sharp Program Analysis and Test Data Generation
Testing is very important in the development of high-quality software systems. A challenge problem in software testing is the design of good test suite. In particular, how can we find a small set of test cases so as to achieve certain coverage criteria? In this talk, I shall describe our work on the automatic generation of test data which satisfy statement and branch coverage, as well as basis path coverage, for the unit testing of C programs. The approach is based on a sharp analysis of the program, which uses symbolic execution and constraint solving techniques. In addition to generating test data, such an analysis can be used to find bugs directly. For example, we have found memory leak problems in some open source code. Finally, I shall briefly mention our work on test data generation for combinatorial testing, which also uses constraint solving techniques.
Reversible Machine Code and Its Abstract Processor Architecture
A reversible abstract machine architecture and its reversible machine code are presented and formalized. For machine code to be reversible, both the underlying control logic and each instruction must be reversible. A general class of machine instruction sets was proven to be reversible, building on our concept of reversible updates. The presentation is abstract and can serve as a guideline for a family of reversible processor designs. By example, we illustrate programming principles for the abstract machine architecture.
Enhancing Modular OO Verification via Separation Logic
Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible.
Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.
Bidirectionalization Transformation Based on Automatic Derivation of Complement Functions
A Bidirectional Transformation is a pair of transformations: a forward transformation and a backward transformation. A forward transformation extracts information from an original data and constructs a new data. The corresponding backward transformation reflects changes on the new data to the original data. Practically useful applications of bidirectional transformations include replicated data synchronization, presentation-oriented structured document development, interactive user interface design, and view updating in the database community. However, developing a bidirectional transformation is hard for the following two reasons.
In this presentation, we tackle the problem using program transformations. Bidirectionalization transformation generates a useful backward transformation from a given forward transformation while guaranteeing that the two transformations satisfy the bidirectional properties. Our transformation is based on a known approach on the problem, called the constant complement approach. Unlike the constant complement approach, our transformation can deal with programs on trees. Moreover, our transformation goes together well with another known approach on the problem, namely the combinator based approach. Our transformation automatically gives the definitions of primitive bidirectional transformations used in the combinator based approach, and we can construct a number of bidirectional transformations thanks to bidirectional combinators.