1. Shin-Chen Mu (Academia Sinica, Taiwan)
An Algebraic Approach to Bi-directional Updating
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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.
Back to the top page