Abstract
A UML Protocol State Machine (PSM) is a behavioral diagram for the specification of the external behavior of a class, interface or component. PSMs have been used in the software development process for different purposes, such as requirements analysis and testing. However, like other UML diagrams, they are often difficult to validate and verify, specially when combined with other artifacts, such as Object Constraint Language (OCL) specifications. This drawback can be overcome by application of an off-the-shelf formal method, namely one supporting automatic validation and verification. Among those, we have the increasingly popular Alloy, based on a simple relational flavor of first-order logic. This paper presents a model transformation from PSMs, optionally complemented with OCL specifications, to Alloy. Not only it enables automatic verification and validation of PSMs, but also a smooth integration of Alloy in current software development practices. © 2012 Springer-Verlag.

Abstract
Lenses are one of the most popular approaches to define bidirectional transformations between data models. However, writing a lens transformation typically implies describing the concrete steps that convert values in a source schema to values in a target schema. In contrast, many XML-based languages allow writing structure-shy programs that manipulate only specific parts of XML documents without having to specify the behavior for the remaining structure. In this paper, we propose a structure-shy bidirectional two-level transformation language for XML Schemas, that describes generic type-level transformations over schema representations coupled with value-level bidirectional lenses for document migration. When applying these two-level programs to particular schemas, we employ an existing algebraic rewrite system to optimize the automatically-generated lens transformations, and compile them into Haskell bidirectional executables. We discuss particular examples involving the generic evolution of recursive XML Schemas, and compare their performance gains over non-optimized definitions. © 2012 Springer-Verlag.

Abstract
Model-Driven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming models from abstract (specifications) to more concrete ones (code). Alloy is an increasingly popular lightweight formal specification language that supports automatic verification. Unfortunately, its widespread industrial adoption is hampered by the lack of an ecosystem of MDE tools, namely code generators. This paper presents a model transformation between Alloy and UML Class Diagrams annotated with OCL. The proposed transformation enables current UML-based tools to also be applied to Alloy specifications, thus unleashing its potential for MDE. © 2011 Springer-Verlag.

Abstract
Defining functions over large, possibly recursive, data structures usually involves a lot of boilerplate. This code simply traverses non-interesting parts of the data, and rapidly becomes a maintainability problem. Many generic programming libraries have been proposed to address this issue. Most of them allow the user to specify the behavior just for the interesting bits of the structure, and provide traversal combinators to "scrap the boilerplate". The expressive power of these libraries usually comes at the cost of efficiency, since runtime checks are used to detect where to apply the type-specific behavior. In previous work we have developed an effective rewrite system for specialization and optimization of generic programs. In this paper we extend it to also cover recursive data types. The key idea is to specialize traversal combinators using well-known recursion patterns, such as folds or paramorphisms. These are ruled by a rich set of algebraic laws that enable aggressive optimizations. We present a type-safe encoding of this rewrite system in Haskell, based on recent language extensions such as type-indexed type families.

Abstract
This paper presents an equational calculus to reason about bidirectional transformations specified in the point-free style. In particular, it focuses on the so-called lenses as a bidirectional idiom, and shows that many standard laws characterising point-free combinators and recursion patterns are also valid in that setting. A key result is that uniqueness also holds for bidirectional folds and unfolds, thus unleashing the power of fusion as a program optimisation technique. A rewriting system for automatic lens optimisation is also presented, to prove the usefulness of the proposed calculus. © 2011 ACM.

Abstract
Various programming languages allow the construction of structure-shy programs. Such programs are defined generically for many different datatypes and only specify specific behavior for a few relevant subtypes. Typical examples are XML query languages that allow selection of subdocuments without exhaustively specifying intermediate element tags. Other examples are languages and libraries for polytypic or strategic functional programming and for adaptive object-oriented programming. In this paper, we present an algebraic approach to transformation of declarative structure-shy programs, in particular for strategic functions and XML queries. We formulate a rich set of algebraic laws, not just for transformation of structure-shy programs, but also for their conversion into structure-sensitive programs and vice versa. We show how subsets of these laws can be used to construct effective rewrite systems for specialization, generalization, and optimization of structure-shy programs. We present a type-safe encoding of these rewrite systems in Haskell which itself uses strategic functional programming techniques. Copyright © 2007 ACM.