title: Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops

authors:
Darion Haase
Kevin Batz
Adrian Gallus
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Lutz Klinkenberg
Tobias Winkler

abstract: A fundamental computational task in probabilistic programming is to infer a program’s output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. While most of the existing literature focuses on statistical approximation, in this paper we address the problem of mathematically exact inference. To achieve this for programs with loops, we rely on a relatively underexplored type of probabilistic loop invariant, which is linked to a loop’s so-called occupation measure . The occupation measure associates program states with their expected number of visits, given the initial distribution. Based on this, we derive the notion of an occupation invariant . Such invariants are essentially dual to probabilistic martingales, the predominant technique for formal probabilistic loop analysis in the literature. A key feature of occupation invariants is that they can take the initial distribution into account and often yield a proof of positive almost sure termination as a by-product. Finally, we present an automatic, template-based invariant synthesis approach for occupation invariants by encoding them as generating functions . The approach is implemented and evaluated on a set of benchmarks.


venue: esop

title: A Program Logic for Under-approximating Worst-case Resource Usage

authors:
Ziyue Jin
Di Wang

abstract: Understanding and predicting the worst-case resource usage is crucial for software quality; however, existing methods either over-approximate with potentially loose bounds or under-approximate without asymptotic guarantees. This paper presents a program logic to under-approximate worst-case resource usage, adapting incorrectness logic (IL) to reason quantitatively about resource consumption. We propose q uantitative f orward and b ackward u nder- a pproximate (QFUA and QBUA) triples, which generalize IL to identify execution paths leading to high resource usage. We also introduce a variant of QBUA that supports reasoning about high-water marks. Our logic is proven sound and complete with respect to a simple IMP-like language, and all meta-theoretical results are mechanized and verified in Rocq. We implement a prototype checker for all three variants of our logic and demonstrate its utility through a few examples and four case studies.


title: Formal Methods meet Digital Twins: Challenges and Opportunities

authors:
Einar Broch Johnsen
Eduard Kamburjan
Andrea Pferscher
Silvia Lizeth Tapia Tarifa

abstract: The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. We may think of digital twins not merely as models, but as systems for model management, integration, and composition. In fact, digital twins are model-centric systems that maintain a two-way connection between an ecosystem of models and the modelled system, realised through streams of observations and streams of interventions. This connection introduces agility as the digital twin can typically both adapt its models on-the-fly to changes in a modelled system and influence the modelled system’s behaviour. In this paper, we discuss key concepts of digital twins from a formal methods perspective and suggest opportunities and challenges for formal methods in digital twin systems. In particular, we consider how formal techniques can be integral to the digital twin, both in terms of digital twin technology and in terms of digital twin models, as well as notions of correctness for the digital twin itself.


title: Causal-Broadcast Memory

authors:
Amir Karniel
Ori Lahav

abstract: We investigate the precise consistency guarantees provided by a simple and prominent distributed implementation of shared memory (a.k.a. key-value store) based on the causal broadcast abstraction. We formalize these guarantees within a weak memory model, which we call “causal-broadcast memory” ( $$\text {CBM}$$ , for short), and relate it to several established weak memory models. In particular, our study reveals that $$\text {CBM}$$ is strictly stronger than “causal memory” consistency, previously proposed to encapsulate the same distributed implementation. Additionally, we address two core verification challenges for $$\text {CBM}$$ : (i) deciding whether a single abstract execution graph is consistent, which we show is solvable in polynomial time, and (ii) verifying reachability of control states for client programs operating atop causal-broadcast memory, which we prove to be undecidable.


title: A Category-Theoretic Framework for Dependent Effect Systems

authors:
Satoshi Kura
Marco Gaboardi
Taro Sekiyama
Hiroshi Unno

abstract: Graded monads refine traditional monads using effect annotations in order to describe quantitatively the computational effects that a program can generate. They have been successfully applied to a variety of formal systems for reasoning about effectful computations. However, existing categorical frameworks for graded monads do not support effects that may depend on program values, which we call dependent effects , thereby limiting their expressiveness. We address this limitation by introducing indexed graded monads , a categorical generalization of graded monads inspired by the fibrational “indexed” view and by classical categorical semantics of dependent type theories. We show how indexed graded monads provide semantics for a refinement type system with dependent effects. We also show how this type system can be instantiated with specific choices of parameters to obtain several formal systems for reasoning about specific program properties. These instances include, in particular, cost analysis, probability-bound reasoning, expectation-bound reasoning, and temporal safety verification.


title: The Memorist Tale: Every Thunk Every Cost All At Once

authors:
Xing Li
Yao Li
Peter Schachte
Christine Rizkallah

abstract: Abstract Lazy evaluation offers great flexibility by computing only what is necessary. However, analysing the cost of lazy programs is notoriously challenging, as computation occurs out of order and depends on future demands. Recent work has proposed alternative semantics for modelling lazy evaluation cost that avoid reasoning about program states. However, existing approaches either rely on nondeterminism or require complex bidirectional semantics. We present the Memorist Semantics , a novel semantics for analysing the cost of lazy programs by explicitly tracking the cost and dependencies of every subterm. Our semantics annotates components of a term with fine-grained cost and usage information, yielding a deterministic semantics that can be expressed through a simple monadic interface. We formalize the semantics in Rocq and verify its soundness with respect to the existing Clairvoyance Semantics. Similar to prior formalized semantics, our semantics is defined for a total, typed language with built-in structural recursion and without support for first-class functions. We outline ideas for possible extensions.


title: Validating Quantum State Preparation Programs

authors:
Liyi Li
Anshu Sharma
Zoukarneini Difaizi Tagba
Sean Frett
Alex Potanin

abstract: One of the key steps in quantum algorithms is to prepare an initial quantum superposition state with distinct features. These state preparation algorithms are essential to the behavior of quantum algorithms, and complicated state preparation algorithms are difficult to program correctly and effectively. We present QSV: a high-assurance framework implemented with the Rocq proof assistant, permitting the development of quantum state preparation programs and validating them to correctly reflect quantum program behaviors. The key is to reduce the program correctness assurance for a program containing a quantum superposition state to that of the program state without superposition. The reduction enables the development of an effective framework for validating quantum state preparation algorithm implementations on a classical computer — a problem considered hard and without a clear solution until now. We utilize the QuickChick property-based testing framework to validate state preparation programs. We evaluated the effectiveness of our approach across 5 case studies implemented using QSV; these cases are not simulatable on current quantum simulators.


title: Modular Automatic Complexity Analysis of Recursive Integer Programs

authors:
Nils Lommen
Jürgen Giesl


title: Lenses for Partially-Specified States

authors:
Kazutaka Matsuda
Minh Nguyen
Meng Wang


title: Denotational reasoning for asynchronous multiparty session types

authors:
Dylan McDermott
Nobuko Yoshida

abstract: We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of communication optimisations, in particular, those involving reordering of messages. Our development crucially relies on modelling message-passing as a computational effect. We apply grading, a paradigm for tracking computational effects, to asynchronous message-passing, demonstrating that multiparty session typing can be viewed as an instance of grading. We demonstrate the utility of our model by showing that it forms an adequate denotational semantics for a call-by-value asynchronous message-passing calculus, that ensures communication safety, deadlock-freedom and liveness in the presence of communication optimisations.


title: Max-Policy Iteration, Revisited

authors:
David Monniaux
Helmut Seidl

abstract: Max-policy iteration is an approach to computing precise numeric program invariants by successive attempts at resolving maximum operators and reduction to mathematical optimization. Mathematical optimization, though, may be expensive. Here, we show, for max-policy iteration on systems of equations over integers as well as over floating point numbers, that mathematical optimization can be replaced by plain value iteration -- which is still guaranteed to terminate. As an application, a precise bound analysis for integer or floating point variables is obtained, avoiding widening operators altogether. We also consider max-policy iteration over the rational numbers, where the right-hand sides are maxima of minima of affine combinations of unknowns. We propose min-policy iteration as an alternative to linear programming for solving the optimization problems posed by max-policy iteration. We prove that max-min policy iteration is guaranteed to return the least solution for bounded systems. We also show how to extend this algorithm to unbounded systems, and how to construct certificates of soundness as well as of optimality of the computed results.


title: A Formal Interface for Concurrent Search Structure Templates

authors:
Duc-Than Nguyen
William Mansky


title: Complete Abstractions for Verification of Polymorphic Functions with Equality

authors:
Malo Revel
Thomas Genet
Thomas P. Jensen


title: Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search

authors:
Yasmin Sarita
Avaljot Singh
Shaurya Gomber
Gagandeep Singh
Mahesh Vishwanathan


title: Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing

authors:
Philipp Schröer
Darion Haase
Joost-Pieter Katoen


title: Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators

authors:
Izumi Tanaka
Ken Sakayori
Shinya Takamaeda-Yamazaki
Naoki Kobayashi


title: Bidirectional Type Checking for Existential Types with Higher-Rank Polymorphism

authors:
Hasti Toossi
Ningning Xie


title: Practical Refinement Session Type Inference

authors:
Toby Ueno
Ankush Das


title: A Formally Verified Procedure for Width Inference in FIRRTL

authors:
Keyin Wang
Xiaomu Shi
Jiaxiang Liu
Zhilin Wu
Fu Song
Taolue Chen
David N. Jansen


title: Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs

authors:
Han Xu
Di Wang


title: Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

authors:
Cheng Zhang
Qiancheng Fu
Hang Ji
Ines Santacruz Del Valle
Alexandra Silva
Marco Gaboardi

abstract: This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.


title: Auditing Rust Crates Effectively

authors:
Lydia Zoghbi
David Thien
Ranjit Jhala
Deian Stefan
Caleb Stanford


venue: gpce

title: Self Reflection for Adaptive Programming

authors:
Giuseppe Attardi
Antonio Cisternino


title: DataScript - A Specification and Scripting Language for Binary Data


title: Memoization in Type-Directed Partial Evaluation

authors:
Vincent Balat
Olivier Danvy

abstract: We use a code generator--type-directed partial evaluation-- to verify conversions between isomorphic types, or more precisely to verify that a composite function is the identity function at some complicated type. A typed functional language such as ML provides a natural support to express the functions and type-directed partial evaluation provides a convenient setting to obtain the normal form of their composition. However, off-the-shelf type-directed partial evaluation turns out to yield gigantic normal forms.We identify that this gigantism is due to redundancies, and that these redundancies originate in the handling of sums, which uses delimited continuations. We successfully eliminate these redundancies by extending type-directed partial evaluation with memoization capabilities. The result only works for pure functional programs, but it provides an unexpected use of code generation and it yields orders-of-magnitude improvements both in time and in space for type isomorphisms.


title: A Protocol Stack Development Tool Using Generative Programming

authors:
Michel Barbeau
Francis Bordeleau


title: Building Composable Aspect-Specific Languages with Logic Metaprogramming

authors:
Johan Brichau
Kim Mens
Kris De Volder


title: Architectural Refactoring in Framework Evolution: A Case Study


title: Towards a Modular Program Derivation via Fusion and Tupling

authors:
Wei-Ngan Chin
Zhenjiang Hu


title: Generative Programming for Embedded Software: An Industrial Experience Report

authors:
Krzysztof Czarnecki
Thomas Bednasch
Peter Unger
Ulrich W. Eisenecker


title: A Framework for the Detection and Resolution of Aspect Interactions

authors:
Rémi Douence
Pascal Fradet
Mario Südholt


title: Aspect-Oriented Modeling: Bridging the Gap between Implementation and Design

authors:
Tzilla Elrad
Omar Aldawud
Atef Bader


title: Program Generation, Termination, and Binding-Time Analysis

authors:
Neil D. Jones
Arne J. Glenstrup


title: Macros That Compose: Systematic Macro Programming


title: Program Termination Analysis in Polynomial Time


title: Generators for Synthesis of QoS Adaptation in Distributed Real-Time Embedded Systems

authors:
Sandeep Neema
Ted Bapty
Jeff Gray
Aniruddha S. Gokhale


title: Optimizing Content Management System Pipelines

authors:
Markus L. Noga
Florian Krüper


title: Component-Based Programming for Higher-Order Attribute Grammars


title: Generative Programming for Embedded Systems

authors:
Janos Sztipanovits
Gabor Karsai


title: Altering Java Semantics via Bytecode Manipulation

authors:
Éric Tanter
Marc Ségura-Devillechaise
Jacques Noyé
José M. Piquer


title: Meta-programming with Concrete Object Syntax


title: Managing Dynamic Changes in Multi-stage Program Generation Systems

authors:
Zhenghao Wang
Richard R. Muntz


title: Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection

authors:
Cristiano Calcagno
Walid Taha
Liwen Huang
Xavier Leroy


title: A Genertative Approach to Framework Instantiation

authors:
Vaclav Cechticky
Philippe Chevalley
Alessandro Pasetti
Walter Schaufelberger


title: An Easy-to-Use Toolkit for Efficient Java Bytecode Translators

authors:
Shigeru Chiba
Muga Nishizawa


title: The Convergence of AOP and Active Databases: Towards Reactive Middleware

authors:
Mariano Cilia
Michael Haupt
Mira Mezini
Alejandro P. Buchmann


title: Component-Based DSL Development


title: Spidle: A DSL Approach to Specifying Streaming Applications

authors:
Charles Consel
Hédi Hamdi
Laurent Réveillère
Lenin Singaravelu
Haiyan Yu
Calton Pu


title: A Journey from Interpreters to Compilers and Virtual Machines


title: Making Patterns Explicit with Metaprogramming


title: Partial Evaluation of MATLAB

authors:
Daniel Elphick
Michael Leuschel
Simon J. Cox


title: An Approach for Supporting Aspect-Oriented Domain Modeling

authors:
Jeff Gray
Ted Bapty
Sandeep Neema
Douglas C. Schmidt
Aniruddha S. Gokhale
Balachandran Natarajan


title: Hume: A Domain-Specific Language for Real-Time Embedded Systems

authors:
Kevin Hammond
Greg Michaelson


title: Concept-Controlled Polymorphism

authors:
Jaakko Järvi
Jeremiah Willcock
Andrew Lumsdaine


title: TDL: A Hardware Description Language for Retargetable Postpass Optimizations and Analyses


title: ANEMIC: Automatic Interface Enabler for Model Integrated Computing

authors:
Steven Nordstrom
Shweta Shetty
Kumar Gaurav Chhokra
Jonathan Sprinkle
Brandon Eames
Ákos Lédeczi


title: DAOP-ADL: An Architecture Description Language for Dynamic Component and Aspect-Based Development

authors:
Mónica Pinto
Lidia Fuentes
José M. Troya


title: A Case for Test-Code Generation in Model-Driven Systems

authors:
Matthew J. Rutherford
Alexander L. Wolf

abstract: A primary goal of generative programming and model-driven development is to raise the level of abstraction at which designers and developers interact with the software systems they are building. During initial development, the benefits of abstraction are clear. However, during testing and maintenance, increased distance from the implementation can be a disadvantage. We view test cases and test harnesses as an essential bridge between the high-level specifications and the implementation. As such, the generation of test cases for fully generated components and test harnesses for partially generated components is of fundamental importance to model-driven systems. In this paper we present our experience with test-case and test-harness generation for a family of model-driven, component-based distributed systems. We describe our development tool, MODEST, and motivate our decision to invest the extra effort needed to generate test code. We present our approach to test-case and test-harness generation and describe the benefits to developers and maintainers of generated systems. Furthermore, we quantify the relative cost of generating test code versus application code and find that the artifact templates for producing test code are simpler than those used for application code. Given the described benefits to developers and maintainers and the relatively low cost of test-code development, we argue that test-code generation should be a fundamental feature of model-driven development efforts.


title: Generating Spreadsheet-Like Tools from Strong Attribute Grammars

authors:
João Saraiva
S. Doaitse Swierstra


title: A Selective, Just-in-Time Aspect Weaver

authors:
Yoshiki Sato
Shigeru Chiba
Michiaki Tatsubori


title: Staged Notational Definitions

authors:
Walid Taha
Patricia Johann


title: Towards a More Piece-ful World


title: On Stage Ordering in Staged Computation


title: SynchNet: A Petri Net Based Coordination Language for Distributed Objects

authors:
Reza Ziaei
Gul Agha


title: An Extension to the Subtype Relationship in C++ Implemented with Template Metaprogramming

authors:
István Zólyomi
Zoltán Porkoláb
Tamás Kozsik


title: A Fresh Calculus for Name Management

authors:
Davide Ancona
Eugenio Moggi


title: A Model-Driven Approach for Smart Card Configuration

authors:
Stéphane Bonnet
Olivier Potonniée
Raphaël Marvie
Jean-Marc Geib


title: Declaring and Enforcing Dependencies Between .NET Custom Attributes

authors:
Vasian Cepa
Mira Mezini


title: Taming Macros

authors:
Ryan Culpepper
Matthias Felleisen


title: A Pointcut Language for Control-Flow

authors:
Rémi Douence
Luc Teboul


title: Model-Driven Configuration and Deployment of Component Middleware Publish/Subscribe Services

authors:
George T. Edwards
Gan Deng
Douglas C. Schmidt
Aniruddha S. Gokhale
Balachandran Natarajan


title: Model-Driven Program Transformation of a Large Avionics Framework

authors:
Jeffrey G. Gray
Jing Zhang
Yuehua Lin
Suman Roychoudhury
Hui Wu
Rajesh Sudarsan
Aniruddha S. Gokhale
Sandeep Neema
Feng Shi
Ted Bapty


title: Software Factories: Assembling Applications with Patterns, Models, Frameworks and Tools


title: Compiling Process Graphs into Executable Code

authors:
Rainer Hauser
Jana Koehler


title: SourceWeave.NET: Cross-Language Aspect-Oriented Programming

authors:
Andrew Jackson
Siobhán Clarke


title: VS-Gen: A Case Study of a Product Line for Versioning Systems

authors:
Jernej Kovse
Christian Gebauer


title: On Designing a Target-Independent DSL for Safe OS Process-Scheduling Components

authors:
Julia L. Lawall
Anne-Françoise Le Meur
Gilles Muller


title: Automatic Remodularization and Optimized Synthesis of Product-Families

authors:
Jia Liu
Don S. Batory


title: Generic Advice: On the Combination of AOP with Generative Programming in AspectC++

authors:
Daniel Lohmann
Georg Blaschke
Olaf Spinczyk


title: Splice: Aspects That Analyze Programs

authors:
Sean McDirmid
Wilson C. Hsieh


title: Modular Language Descriptions


title: Metaphor: A Multi-stage, Object-Oriented Programming Language

authors:
Gregory Neverov
Paul Roe


title: A Generative Approach to the Implementation of Language Bindings for the Document Object Model

authors:
Luca Padovani
Claudio Sacerdoti Coen
Stefano Zacchiroli


title: Meta-programming with Typed Object-Language Representations

authors:
Emir Pasalic
Nathan Linger


title: A Generative Framework for Managed Services

authors:
Liam Peyton
Arif Rajwani


title: Supporting Flexible Object Database Evolution with Aspects

authors:
Awais Rashid
Nicholas A. Leidenfrost


title: A Unification of Inheritance and Automatic Program Specialization


title: Optimising Embedded DSLs Using Template Haskell

authors:
Sean Seefried
Manuel M. T. Chakravarty
Gabriele Keller


title: A Generative Approach to Aspect-Oriented Programming


title: Towards Generation of Efficient Transformations

authors:
Attila Vizhanyo
Aditya Agrawal
Feng Shi


title: Towards a General Template Introspection Library

authors:
István Zólyomi
Zoltán Porkoláb


title: Generating AspectJ Programs with Meta-AspectJ

authors:
David Zook
Shan Shan Huang
Yannis Smaragdakis


title: Sorting Out the Relationships Between Pairs of Iterators, Values, and References


title: Optimizing Marshalling by Run-Time Program Generation

authors:
Baris Aktemur
Joel Jones
Samuel N. Kamin
Lars Clausen


title: On Domain-Specific Languages Reengineering

authors:
Christophe Alias
Denis Barthou


title: abc: The AspectBench Compiler for AspectJ

authors:
Chris Allan
Pavel Avgustinov
Aske Simon Christensen
Laurie J. Hendren
Sascha Kuzins
Jennifer Lhoták
Ondrej Lhoták
Oege de Moor
Damien Sereni
Ganesh Sittampalam
Julian Tibble


title: FeatureC++: On the Symbiosis of Feature-Oriented and Aspect-Oriented Programming

authors:
Sven Apel
Thomas Leich
Marko Rosenmüller
Gunter Saake


title: Generalized Type-Based Disambiguation of Meta Programs with Concrete Object Syntax

authors:
Martin Bravenboer
Rob Vermaas
Jurgen J. Vinju
Eelco Visser


title: Multi-stage Programming with Functors and Monads: Eliminating Abstraction Overhead from Generic Code

authors:
Jacques Carette
Oleg Kiselyov


title: A Generative Programming Approach to Developing DSL Compilers

authors:
Charles Consel
Fabien Latry
Laurent Réveillère
Pierre Cointe


title: Syntactic Abstraction in Component Interfaces

authors:
Ryan Culpepper
Scott Owens
Matthew Flatt


title: Mapping Features to Models: A Template Approach Based on Superimposed Variants

authors:
Krzysztof Czarnecki
Michal Antkiewicz


title: Certifiable Program Generation

authors:
Ewen Denney
Bernd Fischer


title: A Type System for Reflective Program Generators

authors:
Dirk Draheim
Christof Lutteroth
Gerald Weber


title: Implicitly Heterogeneous Multi-stage Programming

authors:
Jason Eckhardt
Roumen Kaiabachev
Emir Pasalic
Kedar N. Swadi
Walid Taha


title: Component-Oriented Programming with Sharing: Containment is Not Ownership

authors:
Daniel Hirschkoff
Tom Hirschowitz
Damien Pous
Alan Schmitt
Jean-Bernard Stefani


title: Statically Safe Program Generation with SafeGen

authors:
Shan Shan Huang
David Zook
Yannis Smaragdakis


title: Applying a Generative Technique for Enhanced Genericity and Maintainability on the J2EE Platform

authors:
Yang Jun
Stan Jarzabek


title: Source-Level Optimization of Run-Time Program Generators

authors:
Samuel N. Kamin
Baris Aktemur
Philip Morton


title: Bossa Nova: Introducing Modularity into the Bossa Domain-Specific Language

authors:
Julia L. Lawall
Hervé Duchesne
Gilles Muller
Anne-Françoise Le Meur


title: Semi-inversion of Guarded Equations


title: Efficient Code Generation for a Domain Specific Language

authors:
Andrew Moss
Henk L. Muller


title: Object-Oriented Reengineering Patterns - An Overview

authors:
Oscar Nierstrasz
Stéphane Ducasse
Serge Demeyer


title: A Generative Programming Approach to Interactive Information Retrieval: Insights and Experiences

authors:
Saverio Perugini
Naren Ramakrishnan


title: Developing Dynamic and Adaptable Applications with CAM/DAOP: A Virtual Office Application

authors:
Mónica Pinto
Daniel Jiménez
Lidia Fuentes


title: Metamodeling Made Easy - MetaEdit+ (Tool Demonstration)


title: Preprocessing Eden with Template Haskell


title: Language Requirements for Large-Scale Generic Libraries

authors:
Jeremy G. Siek
Andrew Lumsdaine


title: A Versatile Kernel for Multi-language AOP

authors:
Éric Tanter
Jacques Noyé


title: Model Compiler Construction Based on Aspect-Oriented Mechanisms

authors:
Naoyasu Ubayashi
Tetsuo Tamai
Shinji Sano
Yusaku Maeno
Satoshi Murakami


title: Shadow Programming: Reasoning About Programs Using Lexical Join Point Information

authors:
Pengcheng Wu
Karl J. Lieberherr


title: AOP++: A Generic Aspect-Oriented Programming Framework in C++

authors:
Zhen Yao
Qilong Zheng
Guoliang Chen


title: Refactoring product lines

authors:
Vander Alves
Rohit Gheyi
Tiago Massoni
Uirá Kulesza
Paulo Borba
Carlos José Pereira de Lucena

abstract: Adoption strategies for Software Product Lines (SPL) frequently involve bootstrapping existing products into a SPL and extending an existing SPL to encompass another product. One way to do that is to use program refactorings. However, the traditional notion of refactoring does not handle appropriately feature models (FM), nor transformations involving multiple instances of the same SPL. For instance, it is not desirable to apply a refactoring into a SPL and reduce its configurability. In this paper, we extend the traditional notion of refactoring to an SPL context. Besides refactoring programs, FMs must also be refactored. We present a set of sound refactorings for FMs. We evaluate this extended refactoring definition for SPL in a real case study in the mobile games domain.


title: When to use features and aspects?: a case study

authors:
Sven Apel
Don S. Batory

abstract: Aspect-Oriented Programming (AOP) and Feature-Oriented Programming (FOP) are complementary technologies that can be combined to overcome their individual limitations. Aspectual Mixin Layers (AML) is a representative approach that unifies AOP and FOP. We use AML in a non-trivial case study to create a product line of overlay networks. We also present a set of guidelines to assist programmers in how and when to use AOP and FOP techniques for implementing product lines in a stepwise and generative manner.


title: Stayin' alert: : moulding failure and exceptions to your needs

authors:
Anya Helene Bagge
Valentin David
Magne Haveraaen
Karl Trygve Kalleberg

abstract: Dealing with failure and exceptional situations is an important but tricky part of programming, especially when reusing existing components. Traditionally, it has been up to the designer of a library to decide whether to use a language's exception mechanism, return values, or other ways to indicate exceptional circumstances. The library user has been bound by this choice, even though it may be inconvenient for a particular use. Furthermore, normal program code is often cluttered with code dealing with exceptional circumstances.This paper introduces an alert concept which gives a uniform interface to all failure mechanisms. It separates the handling of an exceptional situation from reporting it, and allows for retro-fitting this for existing libraries. For instance, we may easily declare the error codes of the POSIX C library for file handling, and then use the library functions as if C had been extended with an exception mechanism for these functions -- a moulding of failure handling to the user's needs, independently of the library designer's choices.


title: YABS: a domain-specific language for pervasive computing based on stigmergy

authors:
Peter Barron
Vinny Cahill

abstract: This paper presents YABS, a novel domain-specific language for defining entity behavior in pervasive computing environments. The programming model of YABS is inspired by nature and, in particular, the observations made by the French biologist Grassé on how social insects coordinate their actions using indirect communication via the environment, a phenomenon that has become known as stigmergy. Following this approach yields a simple yet expressive language that abstracts the complexities of dealing with the variety of underlying technologies typical of pervasive computing environments and that facilitates the incremental construction and improvement of solutions while providing high-level constructs for defining the behavior of entities and their coordination. We show how YABS has been used to program a number of pervasive computing applications both deployed and simulated.


title: Flexible and efficient measurement of dynamic bytecode metrics

authors:
Walter Binder
Jarle Hulaas

abstract: Code instrumentation is finding more and more practical applications, but the required program transformations are often difficult to implement, due to the lack of dedicated, high-level tools. In this paper we present a novel instrumentation framework that supports the partial evaluation of compiled Java code transformation templates, with the goal of efficiently measuring chosen dynamic bytecode and control flow metrics. This framework, as well as the instrumentation code it generates, is implemented in pure Java and hence completely platform-independent. We show the benefits of our approach in several application areas, such as platform-independent resource management and profiling of software components.


title: A verified staged interpreter is a verified compiler

authors:
Edwin C. Brady
Kevin Hammond

abstract: Dependent types and multi-stage programming have both been used, separately, in programming language design and implementation. Each technique has its own advantages --- with dependent types, we can verify aspects of interpreters and compilers such as type safety and stack invariants. Multi-stage programming, on the other hand, can give the implementor access to underlying compiler technology; a staged interpreter is a translator. In this paper, we investigate the combination of these techniques. We implement an interpreter for a simply typed lambda calculus, using dependent types to guarantee correctness properties by construction. We give explicit proofs of these correctness properties, then add staging annotations to generate a translator from the interpreter. In this way, we have constructed a verified compiler from a verified staged interpreter. We illustrate the application of the technique by considering a simple staged interpreter that provides guarantees for some simple resource bound properties, as might be found in a domain specific language for real-time embedded systems.


title: Determining over- and under-constrained systems of equations using structural constraint delta

authors:
David Broman
Kaj Nyström
Peter Fritzson

abstract: Computer aided modeling and simulation of complex physical systems, using components from multiple application domains, such as electrical, mechanical, and hydraulic, have in recent years witnessed a significant growth of interest. In the last decade, equation-based object-oriented (EOO) modeling languages, (e.g. Modelica, gPROMS, and VHDL-AMS) based on acausal modeling using Differential Algebraic Equations (DAEs), have appeared. With such languages, it is possible to model physical systems at a high level of abstraction by using reusable components. A model in an EOO language needs to have the same number of equations as unknowns. A previously unsolved problem concerning this property is the efficient detection of over- or under-constrained models in the case of separately compiled models. This paper describes a novel technique to determine over- and under-constrained systems of equations in models, based on a concept called structural constraint delta. In many cases it is also possible to locate the source of the constraint-problem. Our approach makes use of static type checking and consists of a type inference algorithm. We have implemented it for a subset of the Modelica language, and successfully validated it on several examples.


title: Verifying feature-based model templates against well-formedness OCL constraints

authors:
Krzysztof Czarnecki
Krzysztof Pietroszek

abstract: Feature-based model templates have been recently proposed as a approach for modeling software product lines. Unfortunately, templates are notoriously prone to errors that may go unnoticed for long time. This is because such an error is usually exhibited for some configurations only, and testing all configurations is typically not feasible in practice. In this paper, we present an automated verification procedure for ensuring that no ill-structured template instance will be generated from a correct configuration. We present the formal underpinnings of our proposed approach, analyze its complexity, and demonstrate its practical feasibility through a prototype implementation.


title: A generic annotation inference algorithm for the safety certification of automatically generated code

authors:
Ewen Denney
Bernd Fischer

abstract: Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e., pre- and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains difficult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator).Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property-specific abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding definitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.


title: Concurrent aspects

authors:
Rémi Douence
Didier Le Botlan
Jacques Noyé
Mario Südholt

abstract: Aspect-Oriented Programming (AOP) promises the modularization of so-called crosscutting functionalities in large applications. Currently, almost all approaches to AOP provide means for the description of sequential aspects that are to be applied to a sequential base program. In particular, there is no formally-defined concurrent approach to AOP, with the result that coordination issues between aspects and base programs as well as between aspects cannot precisely be investigated.This paper presents Concurrent Event-based AOP (CEAOP), which addresses this issue. Our contribution can be detailed as follows. First, we formally define a model for concurrent aspects which extends the sequential Event-based AOP approach. The definition is given as a translation into concurrent specifications using Finite Sequential Processes (FSP), thus enabling use of the Labelled Transition System Analyzer (LTSA) for formal property verification. Further, we show how to compose concurrent aspects using a set of general composition operators. Finally, we sketch a Java prototype implementation for concurrent aspects, which generates coordination specific code from the FSP model defining the concurrent AO application.


title: Reflective program generation with patterns

authors:
Manuel Fähndrich
Michael Carbin
James R. Larus

abstract: Runtime reflection facilities, as present in Java and.NET, are powerful mechanisms for inspecting existing code and metadata, as well as generating new code and metadata on the fly. Such power does come at a high price though. The runtime reflection support in Java and.NET imposes a cost on all programs, whether they use reflection or not, simply by the necessity of keeping all metadata around and the inability to optimize code because of future possible code changes. A second—often overlooked—cost is the difficulty of writing correct reflection code to inspect or emit new metadata and code and the risk that the emitted code is not well-formed. In this paper we examine a subclass of problems that can be addressed using a simpler mechanism than runtime reflection, which we call compile-time reflection. We argue for a high-level construct called a transform that allows programmers to write inspection and generation code in a pattern matching and template style, avoiding at the same time the complexities of reflection APIs and providing the benefits of staged compilation in that the generated code and metadata is known to be well-formed and type safe ahead of time.


title: Gaigen 2: a geometric algebra implementation generator

abstract: Geometric Algebra (GA) is an algebra that encodes geometry much better than standard techniques, which are mainly based on linear algebra with various extensions. Compared to standard techniques, GA has clearer semantics and a richer, more consistent language. This expresses itself, among others, in a much greater genericity of functions over the algebra. Exploiting this genericity efficiently is a problem that can be solved through generative programming.This paper describes our Geometric Algebra Implementation Generator Gaigen 2. Gaigen 2 synthesizes highly efficient GA implementations from the specification of the algebra. Functions over such algebras can be defined in a high-level coordinate-free domain-specific language, and Gaigen 2 transforms these functions into low-level coordinate-based code. This code can be emitted in any target language through a custom back-end. Benchmarks of our implementation show that the combination of GA and Gaigen 2 can rival the performance of standard geometry techniques, despite the greater abstraction and genericity of GA.To obtain this high performance, Gaigen 2 must adapt the generated code to the program that links to it. This is done via a profiling feedback loop. While running, the generated code makes a connection to the code generator. The generated code sends information about functions that should be optimized. The code generator registers this information and sends back new type information. After the program terminates, the code is regenerated according to the recorded profile. This profiling feedback technique may also be useful to implement other types of algebras.


title: TCS: a DSL for the specification of textual concrete syntaxes in model engineering

authors:
Frédéric Jouault
Jean Bézivin
Ivan Kurtev

abstract: Domain modeling promotes the description of various facets of information systems by a coordinated set of domain-specific languages (DSL). Some of them have visual/graphical and other may have textual concrete syntaxes. Model Driven Engineering (MDE) helps defining the concepts and relations of the domain by the way of metamodel elements. For visual languages, it is necessary to establish links between these concepts and relations on one side and visual symbols on the other side. Similarly, with textual languages it is necessary to establish links between metamodel elements and syntactic structures of the textual DSL. To successfully apply MDE in a wide range of domains we need tools for fast implementation of the expected growing number of DSLs. Regarding the textual syntax of DSLs, we believe that most current proposals for bridging the world of models (MDE) and the world of grammars (Grammarware) are not completely adapted to this need. We propose a generative solution based on a DSL called TCS (Textual Concrete Syntax). Specifications expressed in TCS are used to automatically generate tools for model-to-text and text-to-model transformations. The proposed approach is illustrated by a case study in the definition of a telephony language.


title: Staging static analyses for program generation

authors:
Sam Kamin
Baris Aktemur
Michael Katelman

abstract: Program generators are most naturally specified using a quote/antiquote facility; the programmer writes programs with holes which are filled in, at program generation time, by other program fragments. If the programs are generated at compile-time, analysis and compilation follow generation, and no changes in the compiler are needed. However, if program generation is done at run time, compilation and analysis need to be optimized so that they will not overwhelm overall execution time. In this paper, we give a compositional framework for defining program analyses which leads directly to a method of staging these analyses. The staging allows the analysis of incomplete programs to be started at compile time; the residual work to be done at run time may be much less costly than the full analysis. We give frameworks for forward and backward analyses, present several examples of specific analyses, and give timing results showing significant speed-ups for the run-time portion of the analysis relative to the full analysis.


title: Software extension and integration with type classes

authors:
Ralf Lämmel
Klaus Ostermann

abstract: The abilities to extend a software module and to integrate a software module into an existing software system without changing existing source code are fundamental challenges in software engineering and programming-language design. We reconsider these challenges at the level of language expressiveness, by using the language concept of type classes, as it is available in the functional programming language Haskell. A detailed comparison with related work shows that type classes provide a powerful framework in which solutions to known software extension and integration problems can be provided. We also pinpoint several limitations of type classes in this context.


title: Roadmap for enhanced languages and methods to aid verification

authors:
Gary T. Leavens
Jean-Raymond Abrial
Don S. Batory
Michael J. Butler
Alessandro Coglio
Kathi Fisler
Eric C. R. Hehner
Cliff B. Jones
Dale Miller
Simon L. Peyton Jones
Murali Sitaraman
Douglas R. Smith
Aaron Stump

abstract: This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.


title: Towards an effective integrated reuse environment

authors:
Jorge Cláudio Cordeiro Pires Mascena
Silvio Romero de Lemos Meira
Eduardo Santana de Almeida
Vinicius Cardoso Garcia

abstract: A fundamental premise for any type of reuse is the knowledge about the existence of the object to be reused. Such knowledge may already be available, for example, due to the past experience of the subject of the reuse action or may be obtained through knowledge dissemination. Information retrieval is a key mechanism for allowing a uniform dissemination of the knowledge about available reusable objects.The instantiation of this problem to the software reuse field is the subject of this work. The synergy among the software reuse and information retrieval fields is exploited in the formulation, implementation and evaluation of an integrated environment that aims at promoting a greater reuse activity level on the quest for developing software with better quality while consuming fewer resources.


title: Creating custom containers with generative techniques

abstract: Component containers are a key part of mainstream component technologies, and play an important role in separating non-functional concerns from the core component logic. This paper addresses two different aspects of containers. First, it shows how generative programming techniques, using AspectC++ and meta-programming, can be used to generate stubs and skeletons without the need for special compilers or interface description languages. Second, the paper describes an approach to create custom containers by composing different non-functional features. Unlike component technologies such as EJB, which only support a predefined set of container types, this approach allows different combinations of non-functional features to be composed in a container to meet the application needs.


title: Expressing heap-shape contracts in linear logic

authors:
Frances Perry
Limin Jia
David Walker

abstract: Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation. In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modified version of LolliMon, a linear logic programming language.


title: Debugging C++ template metaprograms

authors:
Zoltán Porkoláb
József Mihalicza
Ádám Sipos

abstract: Template metaprogramming is an emerging new direction in C++ programming for executing algorithms in compilation time. Despite all of its already proven benefits and numerous successful applications, it is yet to be accepted in industrial projects. One reason is the lack of professional software tools supporting the development of template metaprograms. A strong analogue exists between traditional runtime programs and compile-time metaprograms. This connection presents the possibility for creating development tools similar to those already used when writing runtime programs. This paper introduces Templight, a debugging framework that reveals the steps executed by the compiler during the compilation of C++ programs with templates. Templight's features include following the instantiation chain, setting breakpoints, and inspecting metaprogram information. This framework aims to take a step forward to help template metaprogramming become more accepted in the software industry.


title: Semantic reasoning about feature composition via multiple aspect-weavings

abstract: In this paper, we consider semantic refinement for feature-oriented programming where components are built from features and weavings, which we use to adapt one feature to the context of another one. We address the question of semantic reasoning about multiple weavings. If we know the effect of feature A on X and of feature B on X, what can we conclude about adding both A and B to X? For this, we define conservative weavings which do not modify the state of another feature. We show that composition of several such weavings is however not compositional as it does not preserve semantics. In particular, weavings must consider that other weavings have already been applied. This explains why it is considerably more difficult to reason about multiple aspect weavings. We show criteria on the dependencies between weavings which allow modular, semantics-preserving application of weavings. This is formalized in a calculus for feature composition and also extended to conditional refinements.


title: A graphical programming system for molecular motif search

authors:
Janina Reeder
Robert Giegerich

abstract: We describe a graphical programming system for a domain specific language in biosequence analysis. It supports the development of programs for RNA structure prediction and motif search, created by biologists with little or no programming skills. The system combines several programming paradigms in a productive way. It has a client - server architecture, with a transport layer in XML. The graphical front-end is implemented in the object-oriented paradigm (using Java). Graphics are compiled into a declarative domain-specific language for dynamic programming (ADP) that is embedded in Haskell. Finally, motif search programs expressed in ADP are compiled to imperative code in C, a step which includes substantial domain-specific optimization.


title: Application-specific foreign-interface generation

authors:
John H. Reppy
Chunyan Song

abstract: A foreign interface (FI) mechanism to support interoperability with libraries written in other languages (especially C) is an important feature in most high-level language implementations. Such FI mechanisms provide a Foreign Function Interface (FFI) for the high-level language to call C functions and marshaling and unmarshaling mechanisms to support conversion between the high-level and C data representations. Often, systems provide tools to automate the generation of FIs, but these tools typically lock the user into a specific model of interoperability. It is our belief that the policy used to craft the mapping between the high-level language and C should be distinct from the underlying mechanism used to implement the mapping.In this paper, we describe a FI generation tool, called FIG (for Foreign Interface Generator) that embodies a new approach to the problem of generating foreign interfaces for high-level languages. FIG takes as input raw C header files plus a declarative script that specifies the generation of the foreign interface from the header file. The script sets the policy for the translation, which allows the user to tailor the resulting FI to his or her application. We call this approach application-specific foreign-interface generation. The scripting language uses rewriting strategies as its execution model. The other major feature of the scripting language is a novel notion of composable typemaps that describe the mapping between high-level and low-level types.


title: Assimilating MetaBorg: : embedding language tools in languages

abstract: The MetaBorg usage pattern allows concrete syntax to be associated with application programmer interfaces (API's). Once a concrete syntax is defined, library writers use the Stratego language to write transformations from the concrete syntax to API data and calls in the host language. The result is a compile time translator from the combined host and domain languages to the host language. This translator is not programmable at compile time, and little or none of the infrastructure can be leveraged by a program at run time.These limitations make the MetaBorg pattern difficult or impractical to use in interactive programming. One possibility for adding interactivity to language assimilation is the application of the MetaBorg pattern to Stratego/XT itself. Assimilating language tools into languages, especially dynamic languages, better serves incremental and interactive development. Furthermore, language tool assimilation allows experimentation with language extension at compiler-compile time, compile time, load time and run time.This paper looks at language tool assimilation and makes three contributions. First, it introduces the domain-specific optimization use case as an additional problem that Stratego and related technology might solve. Second, it "partially evaluates" the MetaBorg pattern on the domain-specific languages used in Stratego/XT. Third, and finally, it generalizes the result of the MetaBorg partial evaluation, identifying several applications and application strategies.


title: Distributed meta-programming

authors:
Rui Shi
Chiyan Chen
Hongwei Xi

abstract: Distributed meta-programming (DMP), which allows code to be generated and distributed at run-time, has already become a common practice. However, code generation currently often relies on rather ad hoc approaches that represent code as plain text, making DMP notoriously error-prone. This unfortunate situation is further exacerbated due to issues such as mobility (of code) and locality and heterogeneity (of resources), which complicate testing and debugging drastically.In this paper, we study distributed meta-programming from a type-theoretic perspective, presenting a language to facilitate the construction of programs that may generate and distribute code at run-time. The approach we take makes use of a form of typeful code representation developed in a previous study on meta-programming, and it guarantees statically that only well-typed code (according to some chosen type discipline) can be constructed at run-time and sent to proper locations for execution. We also mention a prototype implementation in support of the practicality of our approach to DMP, providing a solid proof of concept.


title: Safe component updates

authors:
Alexander Stuckenholz
Andre Osterloh

abstract: Component updates always imply the risk of negatively influencing the operability of software systems. Because of wrong combinations of component versions, dependencies might break, methods which do no longer exist, might be called or methods might not be compatible to provided interfaces, objects, or classes. In this paper we model the problem of finding a well-configured system consisting of multiple component versions as a Boolean Optimization Problem. We introduce objective functions and constraints, which use Branch-and-Bound for restricting the search space and yield most recent, minimal systems.


title: Transparent program transformationsin the presence of opaque code

authors:
Eli Tilevich
Yannis Smaragdakis

abstract: User-level indirection is the automatic rewriting of an application to interpose code that gets executed upon program actions such as object field access, method call, object construction, etc. The approach is constrained by the presence of opaque (native) code that cannot be indirected and can invalidate the assumptions of any indirection transformation. In this paper, we demonstrate the problem of employing user-level indirection in the presence of native code. We then suggest reasonable assumptions on the behavior of native code and a simple analysis to compute the constraints they entail. We show that the type information at the native code interface is often a surprisingly sufficient approximation of native behavior for heuristically estimating when user-level indirection can be applied safely. Furthermore, we introduce a new user-level indirection approach that minimizes the constraints imposed by interactions with native code.


title: Feature refactoring a multi-representation program into a product line

authors:
Salvador Trujillo
Don S. Batory
Oscar Díaz

abstract: Feature refactoring is the process of decomposing a program into aset of modules, called features, that encapsulate increments in program functionality. Different compositions of features yield different programs. As programs are defined using multiple representations, such as code, makefiles, and documentation, feature refactoring requires all representations to be factored. Thus, composing features produces consistent representations of code, make files, documentation, etc. for a target program. We present acase study of feature refactoring a substantial tool suite that usesmultiple representations. We describe the key technical problems encountered, and sketch the tool support needed for simplifying such refactorings in the future.


title: A multi-stage language with intensional analysis

authors:
Marcos Viera
Alberto Pardo

abstract: This paper presents the definition of a language with reflection primitives. The language is a homogeneous multi-stage language that provides the capacity of code analysis by the inclusion of a pattern matching mechanism that permits inspection of the structure of quoted expressions and their destruction into component subparts. Quoted expressions include an explicit annotation of their context which is used for dynamic inference of type, where a dynamic typing discipline based on Hinze and Cheney's approach is used for typing quoted expressions.This paper follows the approach of Sheard and Pasalic about the use of the meta-language Ωmega as a tool for language design. In this sense, it is shown how to represent the syntax, the static as well as the dynamic semantics of the proposed language in terms of Ωmega constructs.


title: Patches as better bug reports

abstract: Tools and analyses that find bugs in software are becoming increasingly prevalent. However, even after the potential false alarms raised by such tools are dealt with, many real reported errors may go unfixed. In such cases the programmers have judged the benefit of fixing the bug to be less than the time cost of understanding and fixing it.The true utility of a bug-finding tool lies not in the number of bugs it finds but in the number of bugs it causes to be fixed.Analyses that find safety-policy violations typically give error reports as annotated backtraces or counterexamples. We propose that bug reports additionally contain a specially-constructed patch describing an example way in which the program could be modified to avoid the reported policy violation. Programmers viewing the analysis output can use such patches as guides, starting points, or as an additional way of understanding what went wrong.We present an algorithm for automatically constructing such patches given model-checking and policy information typically already produced by most such analyses. We are not aware of any previous automatic techniques for generating patches in response to safety policy violations. Our patches can suggest additional code not present in the original program, and can thus help to explain bugs related to missing program elements. In addition, our patches do not introduce any new violations of the given safety policy.To evaluate our method we performed a software engineering experiment, applying our algorithm to over 70 bug reports produced by two off-the-shelf bug-finding tools running on large Java programs. Bug reports also accompanied by patches were three times as likely to be addressed as standard bug reports.This work represents an early step toward developing new ways to report bugs and to make it easier for programmers to fix them. Even a minor increase in our ability to fix bugs would be a great increase for the quality of software.


title: A dynamic aspect-oriented system for OS kernels

authors:
Yoshisato Yanagisawa
Kenichi Kourai
Shigeru Chiba

abstract: We propose a dynamic aspect-oriented system for operating system (OS) kernels written in the C language. Unlike other similar systems, our system named KLASY allows the users to pointcut not only function calls but also member accesses to structures. This feature helps the developers who want to use aspects for profiling or debugging an OS kernel. To enable this, KLASY uses a modified C compiler for compiling an OS kernel. The modified compiler produces extended symbol information, which enables a dynamic weaver to find the memory addresses of join point shadows during runtime. Since a normal C compiler produces only limited symbol information, other dynamic aspect-oriented systems for C have been able to pointcut only function calls. We have implemented KLASY for Linux with the GNU C compiler. Our experiments revealed that KLASY achieves sufficient execution performance for practical use. Our case studies disclosed that KLASY is useful for real applications.


title: Repleo: a syntax-safe template engine

authors:
Jeroen Arnoldus
Jeanot Bijpost
Mark van den Brand

abstract: Templates are a very common solution to generate code. They are used for different tasks like rendering webpages, creating Java Beans and so on. Most template systems have no notion of the object language and just generate text. The drawback of this approach is the possibility to generate syntactical incorrect code. This can lead to all kinds of annoying errors.


title: Preventing injection attacks with syntax embeddings

authors:
Martin Bravenboer
Eelco Dolstra
Eelco Visser

abstract: Software written in one language often needs to construct sentences in another language, such as SQL queries, XML output, or shell command invocations. This is almost always done using unhygienic string manipulation, the concatenation of constants and client-supplied strings. A client can then supply specially crafted input that causes the constructed sentence to be interpreted in an unintended way, leading to an injection attack. We describe a more natural style of programming that yields code that is impervious to injections by construction. Our approach embeds the grammars of the guest languages (e.g., SQL) into that of the host language (e.g., Java) and automatically generates code that maps the embedded language to constructs in the host language that reconstruct the embedded sentences, adding escaping functions where appropriate. This approach is generic, meaning that it can be applied with relative ease to any combination of host and guest languages.


title: Debugging macros

authors:
Ryan Culpepper
Matthias Felleisen

abstract: Over the past two decades, Scheme macros have evolved into a powerful API for the compiler front-end. Like Lisp macros, their predecessors, Scheme macros expand source programs into a small core language; unlike Lisp systems, Scheme macro expanders preserve many desirable properties, including lexical scope and source location. Using such macros, Scheme programmers now routinely develop the ultimate abstraction: embedded domain-specific programming languages.


title: Aspects of availability

authors:
Pascal Fradet
Stéphane Hong Tuan Ha

abstract: International audience


title: Simple and safe SQL queries with c++ templates

authors:
Joseph Gil
Keren Lenz

abstract: Most software applications use a relational database for data man-agement and storage. Interaction with such a database is often done by letting the program construct strings with valid SQL statements, which are then sent for execution to the database engine. The fact that these statements are only checked for correctness at runtime is a source for many potential problems such as type and syntax errors and vulnerability to injection attacks. The ARARAT system presented here offers a method for dealing with these predicaments, by coercing the host C++ compiler to do the necessary checks of the generated strings. A library of templates (and preprocessor directives) effectively extends C++ with a little language representing an augmented relational algebra formalism. Type checking of this language extension, as done by the template library, assures, at compile-time, the correctness of the generated SQL strings. All SQL statements constructed by the system are immune to injection attacks. Standard techniques (e.g., “expression templates”) for compile time representation of symbolic structures, are enhanced by our system to support a type system and a symbol table lookup of the symbolic structure. Our work may also open the way for embed-ding other domain specific languages in C++. 1.


title: Library composition and adaptation using c++ concepts

authors:
Jaakko Järvi
Matthew A. Marcus
Jacob N. Smith

abstract: Large scale software is composed of libraries produced by different entities. Non-intrusive and efficient mechanisms for adapting data structures from one library to conform to APIs of another are essential for the success of large software projects. Concepts and concept maps, planned features for the next version of C++, have been designed to support adaptation, promising generic, non-intrusive, efficient, and identity preserving adapters. This paper analyses the use of concept maps for library composition and adaptation, comparing and contrasting concept maps to other common adaptation mechanisms. We report on two cases of data structure adaptation between different libraries, indicating best practices and idioms along the way. First, we adapt GUI controls from several frameworks for use with a generic layout engine, extending the application of concepts to run-time polymorphism. Second, we develop a transparent adaptation layer between an image processing library and a graph algorithm library, enabling the efficient application of graph algorithms to the image processing domain.


title: A type-centric framework for specifying heterogeneous, large-scale, component-oriented, architectures

authors:
Georg Jung
John Hatcliff

abstract: Maintaining integrity, consistency, and enforcing conformance in architectures of large-scale systems requires specification and enforcement of many different forms of structural constraints. While type systems have proved effective for enforcing structural constraints in programs and data structures, most architectural modeling frameworks include only weak notions of typing or rely on first-order logic constraint languages that have steep learning curves and that become unwieldy when scaling to large systems.


title: Lightweight scalable components

authors:
Tetsuo Kamina
Tetsuo Tamai

abstract: One limitation of the well-known family polymorphism approach is that each "family" will be a large monolithic program. In this paper, we introduce a minimal lightweight set of language features that treat each member of a family as a reusable programming unit, while preserving the important feature of scalability. The only one language construct we propose in this paper is type parameter members, which allows type parameters to be referred from the outside of class declarations. To investigate properties of type parameter members in the real programming language settings, we develop a programming language Scalable Java (SJ), an extension of Java generics with type parameter members. To carefully investigate the type soundness of SJ, we develop FGJ#, a core calculus of this extension based on FGJ, a functional core of Java with generics. Furthermore, to explore how to implement this proposal, we define the erasure of FGJ# programs as an extension of the erasure of FGJ programs, which compiles SJ to Java without generics.


title: Seamless development of software product lines

authors:
Miguel A. Laguna
Bruno González-Baixauli
José M. Marqués

abstract: One of the key problems in the development of software product lines is the representation and management of variability and commonality. The customary way to define both aspects is by means of feature models that also allow the configuration of each specific application within the product line to be selected. However the control of traceability between the features and the architectural models (generally based on UML) is not simple. The fundamental reasons are the complexity of the traceability relationships, and the fact that the same modeling mechanisms (e.g., the specialization in a class diagram) serve to express the variation points in the models that represent the product line and in each specific application. The aim of this work is to use the package merge mechanism of the UML 2 infrastructure meta-model as the representation (and support for the configuration) of the variability in the product line while reserving the classical mechanisms (the specialization in the structural models, the < > relationship in the use case models, etc.) to express the variants in execution time of each specific application. The structure of the feature models is directly reflected in the relationships between packages in the architectural models, so the traceability of the configuration decisions is straightforward. The direct implementation of the package merge mechanism using the facility of partial classes of languages such as C# is an additional advantage that leads to the ideal of "seamless development".


title: Oz/K: a kernel language for component-based open programming

authors:
Michael Lienhardt
Alan Schmitt
Jean-Bernard Stefani

abstract: Programming in an open environment remains challenging because it requires combining modularity, security, concurrency, distribution, and dynamicity. In this paper, we propose an approach to open distributed programming that exploits the notion of locality, which has been used in the past decade as a basis for several distributed process calculi such as Mobile Ambients, Dπ, and Seal. We use the locality concept as a form of component that serves as a unit of modularity, of isolation, and of passivation. Specifically, we introduce in this paper Oz/K, a kernel programming language, that adds to the Oz computation model a notion of locality borrowed from the Kell calculus. We present an operational semantics for the language and several examples to illustrate how Oz/K supports open distributed programming.


title: 42: programmable models of computation for a component-based approach to heterogeneous embedded systems

authors:
Florence Maraninchi
Tayeb Bouhadiba

abstract: Every notion of a component for the development of embedded systems has to take heterogeneity into account: components may be hardware or software or OS, synchronous or asynchronous, deterministic or not, detailed w.r.t. time or not, detailed w.r.t. data or not, etc. A lot of approaches, following Ptolemy, propose to define several 'Models of Computation and Communication' (MoCCs) to deal with heterogeneity, and a framework in which they can be combined hierarchically.


title: Open multi-methods for c++

authors:
Peter Pirkelbauer
Yuriy Solodkyy
Bjarne Stroustrup

abstract: Multiple dispatch - the selection of a function to be invoked based on the dynamic type of two or more arguments - is a solution to several classical problems in object-oriented programming. Open multi-methods generalize multiple dispatch towards open-class extensions, which improve separation of concerns and provisions for retroactive design. We present the rationale, design, implementation, and performance of a language feature, called open multi-methods, for C++. Our open multi-methods support both repeated and virtual inheritance. Our call resolution rules generalize both virtual function dispatch and overload resolution semantics. After using all information from argument types, these rules can resolve further ambiguities by using covariant return types. Great care was taken to integrate open multi-methods with existing C++ language features and rules. We describe a model implementation and compare its performance and space requirements to existing open multi-method extensions and workaround techniques for C++. Compared to these techniques, our approach is simpler to use, catches more user mistakes, and resolves more ambiguities through link-time analysis, runs significantly faster, and requires less memory. In particular, the runtime cost of calling an open multi method is constant and less than the cost of a double dispatch (two virtual function calls). Finally, we provide a sketch of a design for open multi-methods in the presence of dynamic loading and linking of libraries.


title: Can we teach computers to write fast libraries?

abstract: As the computing world "goes multicore", high performance library development finally becomes a nightmare. Optimal programs, and their underlying algorithms, have to be adapted to take full advantage of the platform's parallelism, memory hierarchy, and available instruction set. To make things worse, the best implementations are often platform-dependent and platforms are constantly evolving, which quickly renders libraries obsolete. As a consequence, developers are forced to permanently re-implement and re-optimize the same functionality and often even revert to assembly coding just as 50 years ago.


title: Refactoring-based support for binary compatibility in evolving frameworks

authors:
Ilie Savga
Michael Rudolf

abstract: The evolution of a software framework may invalidate existing plugins - modules that used one of its previous versions. To preserve binary compatibility (i.e., plugins will link and run with a new framework release without recompilation), we automatically create an adaptation layer that translates between plugins and the framework. The creation of these adapters is guided by information about syntactic framework changes (refactorings). For each supported refactoring we formally define a comeback - a refactoring used to construct adapters. For an ordered set of refactorings that occured between two framework versions, the backward execution of the corresponding comebacks yields the adaptation layer.


title: Challenges in generating qos-constrained software implementations

abstract: The limited processing power and memory capacities of early computing technologies often forced designers of real-time and embedded software to devise relatively sophisticated and complex architectural and programming patterns. The primary motivation, of course, was to eke out as much capability as the underlying implementation technologies could provide. Unfortunately, this tended to add complexity to the software, often making it very difficult to evolve, maintain, or port to different (e.g., more advanced) technologies. One of the primary sources of complexity in such systems is the intricate interleaving of application-specific concerns with implementation concerns that prevents easy distinction of one from the other.


title: Safe composition of product lines

authors:
Sahil Thaker
Don S. Batory
David Kitchin
William R. Cook

abstract: Programs of a software product line can be synthesized by composing modules that implement features. Besides high-level domain constraints that govern the compatibility of features, there are also low-level implementation constraints: a feature module can reference elements that are defined in other feature modules. Safe composition is the guarantee that all programs in a product line are type safe: i.e., absent of references to undefined elements (such as classes, methods, and variables). We show how safe composition properties can be verified for AHEAD product lines using feature models and SAT solvers.


title: Generative metaprogramming

authors:
Salvador Trujillo
Maider Azanza
Oscar Díaz

abstract: Recent advances in Software Engineering have reduced the cost of coding programs at the expense of increasing the complexity of program synthesis, i.e. metaprograms, which when executed, will synthesize a target program. The traditional cycle of configuring-linking-compiling, now needs to be supplemented with additional transformation steps that refine and enhance an initial specification until the target program is obtained. So far, these synthesis processes are based on error-prone, hand-crafted scripting. To depart from this situation, this paper addresses generative metaprogramming, i.e. the generation of program-synthesis metaprograms from declarative specifications. To this end, we explore (i) the (meta) primitives for program synthesis, (ii) the architecture that dictates how these primitives can be intertwined, and (iii) the declarative specification of the metaprogram from which the code counterpart is generated.


title: Parsimony principles for software components and metalanguages

abstract: Software is a communication system. The usual topic of communication is program behavior, as encoded by programs. Domain-specific libraries are codebooks, domain-specific languages are coding schemes, and so forth. To turn metaphor into method, we adapt tools from information theory - the study of efficient communication - to probe the efficiency with which languages and libraries let us communicate programs. In previous work we developed an information-theoretic analysis of software reuse in problem domains. This new paper uses information theory to analyze tradeoffs in the design of components, generators, and metalanguages. We seek answers to two questions: (1) How can we judge whether a component is over- or under-generalized? Drawing on minimum description length principles, we propose that the best component yields the most succinct representation of the use cases. (2) If we view a programming language as an assemblage of metalanguages, each providing a complementary style of abstraction, how can these metalanguages aid or hinder us in efficiently describing software? We describe a complex triangle of interactions between the power of an abstraction mechanism, the amount of reuse it enables, and the cognitive difficulty of its use.


title: Constructing language processors with algebra combinators

authors:
Philip Weaver
Garrin Kimmell
Nicolas Frisby
Perry Alexander

abstract: Modular Monadic Semantics (MMS) is a well-known mechanism for structuring modular denotational semantic definitions for programming languages. The principal attraction of MMS is that families of language constructs can be independently specified and later combined in a mix-and-match fashion to create a complete language semantics. This has proved useful for constructing formal, yet executable, semantics when prototyping languages. In this work we demonstrate that MMS has an additional software engineering benefit. Rather than composing semantics for various language constructs, we can use MMS to compose various differing semantics for the same language constructs. We describe algebra combinators, the principal vehicle for achieving this reuse, along with a series of applications of the technique for common language processing tasks.


title: Generative programming techniques for Java library migration

authors:
Victor L. Winter
Azamatbek Mametjanov

abstract: Embedded systems can be viewed as scaled-down versions of their stand-alone counterparts. In many cases, the software abstractions and libraries for embedded systems can be derived from libraries for stand-alone systems. One such example is the Java library for Java Virtual Machines. An embedded system does not always support all features as in the case of an embedded JVM that does not support floating-point operations. In such cases, an existing library needs to be migrated to the embedded platform. Libraries are large collections of code and manual migration is a daunting task. In this paper, we provide an automated approach to the library migration problem using program transformations. The solution developed in this paper enables rapid adaptation and re-targeting of Java libraries in the presence of evolving libraries and evolving embedded platforms.


title: Context-aware scanning for parsing extensible languages

authors:
Eric Van Wyk
August Schwerdfeger

abstract: This paper introduces new parsing and context-aware scanning algorithms in which the scanner uses contextual information to disambiguate lexical syntax. The parser uses a slightly modified LR-style algorithm that passes to the scanner the set of valid symbols that the scanner may return at that point in parsing. This set is those terminals whose entries in the parse table for the current parse state are shift, reduce, or accept, but not error. The scanner then only returns tokens in this set. An analysis is given that can statically verify that the scanner will never return more than one token for a single input. Context-aware scanning is especially useful when parsing and scanning extensible languages in which domain specific languages can be embedded. It has been used in extensible versions of Java 1.4 and ANSI C. We illustrate this approach with a declarative specification of a subset of Java and extensions that embed SQL queries and Boolean expression tables into Java.


title: Program refactoring using functional aspects

authors:
Sven Apel
Christian Kästner
Don S. Batory

abstract: A functional aspect is an aspect that has the semantics of a transformation; it is a function that maps a program to an advised program. Functional aspects are composed by function composition. In this paper, we explore functional aspects in the context of aspect-oriented refactoring. We show that refactoring legacy applications using functional aspects is just as flexible and expressive as traditional aspects (functional aspects can be refactored in any order), while having a simpler semantics (aspect composition is just function composition), and causes fewer undesirable interactions between aspects (the number of potential interactions between functional aspects is half the number of potential interactions between traditional aspects). We analyze several aspect-oriented programs of different sizes to support our claims.


title: Feature featherweight java: a calculus for feature-oriented programming and stepwise refinement

authors:
Sven Apel
Christian Kästner
Christian Lengauer

abstract: Feature-oriented programming (FOP) is a paradigm that incorporates programming language technology, program generation techniques, and stepwise refinement. In their GPCE'07 paper, Thaker et al. suggest the development of a type system for FOP to guarantee safe feature composition, i.e, to guarantee the absence of type errors during feature composition. We present such a type system along with a calculus for a simple feature-oriented, Java-like language, called Feature Featherweight Java (FFJ). Furthermore, we explore four extensions of FFJ and how they affect type soundness.


title: Using modern mathematics as an FOSD modeling language

abstract: Modeling languages are a fundamental part of automated software development. MDD, for example, uses UML class diagrams and state machines as languages to define applications. In this paper, we explore how Feature Oriented Software Development (FOSD) uses modern mathematics as a modeling language to express the design and synthesis of programs in software product lines, but demands little mathematical sophistication from its users. Doing so has three practical benefits: (1) it offers a simple and principled mathematical description of how FOSD transforms, derives, and relates program artifacts, (2) it exposes previously unrecognized commuting relationships among tool chains, thereby providing new ways to debug tools, and (3) it reveals new ways to optimize software synthesis.


title: Generating customized verifiers for automatically generated code

authors:
Ewen Denney
Bernd Fischer

abstract: Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations.


title: Emerging challenges for large scale systems integration

abstract: Over the past 15 years large systems integrators have grown in size by an order of magnitude. During this time the nature of the systems we build, the manner in which they are built, and the clients for whom they are built have seen corresponding growth. During this talk I will review some of these changes and discuss some of the challenges we see on the horizon as these trends continue. What kind of systems would a systems integrator with 2 million people develop? How would they be built?


title: Integrating semantics and compilation: using c++ concepts to develop robust and efficient reusable libraries

authors:
Peter Gottschling
Andrew Lumsdaine

abstract: Concepts are a recently proposed extension to C++ for the direct linguistic support of generic programming. As the interface description mechanism for large-scale generic libraries, concepts do not exist in isolation, but rather in semantic frameworks (or concept lattices). Concepts provide powerful type-checking capabilities for generic programming and the semantics associated with them present new and interesting capabilities for library-compiler interactions. This paper presents some of these emergent capabilities in the context of a library of algebraic concepts. Based on this library, which possesses rich, well-structured and mathematically-based semantics, we demonstrate how the concepts therein can enable a sophisticated oncept-aware design for a broad range of scientific generic libraries. In particular, we show that concepts can enable the description and application of property-based, library-defined, optimizations. Whereas compilers without concepts are limited to optimization of built-in types, library-defined optimizations based on concepts not only allow for optimizations of user-defined types unknown to the compiler, they are even applicable to types unknown to the library developer.


title: Polymorphic embedding of dsls

authors:
Christian Hofer
Klaus Ostermann
Tillmann Rendel
Adriaan Moors

abstract: The influential pure embedding methodology of embedding domain-specific languages (DSLs) as libraries into a general-purpose host language forces the DSL designer to commit to a single semantics. This precludes the subsequent addition of compilation, optimization or domain-specific analyses. We propose polymorphic embedding of DSLs, where many different interpretations of a DSL can be provided as reusable components, and show how polymorphic embedding can be realized in the programming language Scala. With polymorphic embedding, the static type-safety, modularity, composability and rapid prototyping of pure embedding are reconciled with the flexibility attainable by external toolchains.


title: Property models: from incidental algorithms to reusable components

authors:
Jaakko Järvi
Mat Marcus
Sean Parent
John Freeman
Jacob N. Smith

abstract: A user interface, such as a dialog, assists a user in synthesising a set of values, typically parameters for a command object. Code for "command parameter synthesis" is usually application-specific and non-reusable, consisting of validation logic in event handlers and code that controls how values of user interface elements change in response to a user's actions, etc. These software artifacts are incidental - they are not explicitly designed and their implementation emerges from a composition of locally defined behaviors.


title: Lightweight dependent classes

authors:
Tetsuo Kamina
Tetsuo Tamai

abstract: Extensive research efforts have been devoted to implement a group of type-safe mutually recursive classes; recently, proposals for separating each member of the group as a reusable and composable programming unit have also been presented. One problem of these proposals is verbosity of the source programs; we have to declare a recursive type parameter to parameterize each mutually recursive class within each class declaration, and we have to declare a fixed-point class with empty class body for each parameterized class. Therefore, even though the underlying type system is simple, programs written in these languages tend to be rather complex and hard to understand. In this paper, we propose a language with lightweight dependent classes that forms a simple type system built on top of generic Java. In this language, we can implement each member of type-safe mutually recursive classes in a separate source file without writing a lot of complex boilerplate code. To carefully investigate type soundness of our proposal, we develop X.FGJ, a simple extension of FGJ supporting lightweight dependent classes. This type system is proved to be sound.


title: On the modularity of feature interactions

authors:
Chang Hwan Peter Kim
Christian Kästner
Don S. Batory

abstract: Feature modules are the building blocks of programs in software product lines (SPLs). A foundational assumption of feature-based program synthesis is that features are composed in a predefined sequence called a natural order. Recent work on virtual separation of concerns reveals a new model of feature interactions that shows that feature modules can be quantized as compositions of smaller modules called derivatives. We present this model and examine some of its consequences, namely, that (1) a given program can be reconstructed by composing features in any order, and (2) the contents of a feature module (as expressed as a composition of derivatives) is determined automatically by a feature order. We show that different orders allow one to adjust the contents of a feature module to isolate and study the impact of interactions that a feature has with other features. We also show the utility of generalizing safe composition (SC), a basic analysis of SPLs that verifies program type-safety, to demonstrate that every legal composition of derivatives (and thus any composition order of features) produces a type-safe program, which is a much stronger SC property.


title: An abstraction for reusable MDD components: model-based generation of model-based code generators

authors:
Vinay Kulkarni
Sreedhar Reddy

abstract: We discuss our experience of using model-based techniques to generate model-based code generators. The central idea behind model-driven development (MDD) is to use suitable models to specify various concerns and transform these models to a variety of text artifacts. A business product needs to deliver a given business functionality on a wide variety of implementation platforms and architectures thus necessitating multiple sets of code generators. However, there is a considerable commonality across these code generators. In absence of a suitable abstraction for capturing this commonality, there is little or no reuse across these code generators. We present an abstraction for organizing model-based code generators as a hierarchical composition of reusable building blocks. A building block is a localized specification of a concern in terms of a concern-specific meta model, model to model trans-formation, and model to text transformation. Model-based code generation is a 3-step walk over the composition tree wherein the first step transforms individual concern-specific models into a unified model, the second step transforms the unified model into individual concern-specific text artifacts, and the third step composes these text artifacts.


title: Typing communicating component assemblages

authors:
Michael Lienhardt
Alan Schmitt
Jean-Bernard Stefani

abstract: Building complex component-based software architectures can lead to subtle assemblage errors. In this paper, we introduce a type-system-based approach to avoid message handling errors when assembling component-based communication systems. Such errors are not captured by classical type systems of host programming languages such as Java or ML. Our approach relies on the definition of a small process calculus that captures the operational essence of our target component-based framework for communication systems, and on the definition of a novel type system that combines row types with process types.


title: Fundamentalist functional programming

abstract: In 1984, John Hughes wrote a seminal paper titled, "Why Functional Programming Matters," in which he eloquently explained the value of pure and lazy functional programming. Due to the increasing importance of the Web and the introduction of many-core machines, in the quarter of a century since the paper was written, the problems associated with imperative languages and their side effects have become increasingly evident. This talk argues that fundamentalist functional programming-that is, radically eliminating all side effects from programming languages, including strict evaluation-is what it takes to conquer the concurrency and parallelism dragon. Programmers must embrace pure, lazy functional programming "all the way"-with all effects apparent in the type system of the host language using monads. A radical paradigm shift is the answer, but does that mean that all current programmers will be lost along the way? Fortunately not! By design, LINQ is based on monadic principles, and the success of LINQ proves that the world does not fear the monads.


title: Efficient compilation techniques for large scale feature models

authors:
Marcílio Mendonça
Andrzej Wasowski
Krzysztof Czarnecki
Donald D. Cowan

abstract: Feature modeling is used in generative programming and software product-line engineering to capture the common and variable properties of programs within an application domain. The translation of feature models to propositional logics enabled the use of reasoning systems, such as BDD engines, for the analysis and transformation of such models and interactive configurations. Unfortunately, the size of a BDD structure is highly sensitive to the variable ordering used in its construction and an inappropriately chosen ordering may prevent the translation of a feature model into a BDD representation of a tractable size. Finding an optimal order is NP-hard and has for long been addressed by using heuristics.


title: Pantaxou: a domain-specific language for developing safe coordination services

authors:
Julien Mercadal
Nicolas Palix
Charles Consel
Julia L. Lawall

abstract: Coordinating entities in a networked environment has always been a significant challenge for software developers. In recent years, however, it has become even more difficult, because devices have increasingly rich capabilities, combining an ever larger range of technologies (networking, multimedia, sensors, etc.).


title: Code generation to support static and dynamic composition of software product lines

authors:
Marko Rosenmüller
Norbert Siegmund
Gunter Saake
Sven Apel

abstract: Software product lines (SPLs) are used to create tailor-made software products by managing and composing reusable assets. Generating a software product from the assets of an SPL is possible statically before runtime or dynamically at load-time or runtime. Both approaches have benefits and drawbacks with respect to composition flexibility, performance, and resource consumption. Which type of composition is preferable should be decided by taking the application scenario into account. Current tools and languages, however, force a programmer to decide between static and dynamic composition during development. In this paper, we present an approach that employs code generation to support static and dynamic composition of features of a single code base. We offer an implementation on top of FeatureC++, an extension of the C++ programming language that supports software composition based on features. To simplify dynamic composition and to avoid creation of invalid products we furthermore provide means to (1) validate the correctness of a composition at runtime, (2) automatically instantiate SPLs in case of stand-alone applications, and (3) automatically apply interaction code of crosscutting concerns.


title: Generating incremental implementations of object-set queries

authors:
Tom Rothamel
Yanhong A. Liu

abstract: High-level query constructs help greatly improve the clarity of programs and the productivity of programmers, and are being introduced to increasingly more languages. However, the use of high-level queries in programming languages can come at a cost to program efficiency, because these queries are expensive and may be computed repeatedly on slightly changed inputs. For efficient computation in practical applications, a powerful method is needed to incrementally maintain query results with respect to updates to query parameters.