Theses

Macedo N.  2014.  A Relational Approach to Biditectional Transformations. Abstractphd14nmm.pdf

Transforming data between different formats is an essential task in computer science and software engineering. Ordinary as this exercise may seem, creating a target artifact from a source artifact a is often just the first step in a dynamic evolution process: the initial transformation implicitly binds a and b, and as either artifact gets updated, modifications must be propagated to the other side in order to keep the overall system consistent. For decades, this kind of problem has been addressed via ad hoc or domainspecific techniques in virtually every area of computer science—the view-update problem from the database community being the classic example. However, in the last few years, research on bidirectional transformation (Czarnecki et al., 2009) has exploded, with developments in areas like heterogeneous data synchronization (Brabrand et al., 2005; Kawanaka and Hosoya, 2006; Foster et al., 2007), string manipulation (Bohannon et al., 2008; Barbosa et al., 2010), functional languages (Matsuda et al., 2007; Voigtländer, 2009; Pacheco and Cunha, 2010), model transformation (Ehrig et al., 2007; Cicchetti et al., 2010; Macedo and Cunha, 2013), user interfaces (Meertens, 1998; Huet al., 2008), relational databases (Bancilhon and Spyratos, 1981; Dayal and Bernstein,1982; Bohannon et al., 2006), graph transformation (Schürr, 1994; Hidaka et al., 2010), or spreadsheet systems (Cunha et al., 2012; Macedo et al., 2014c). The main idea behind bidirectional transformation frameworks is having a single transformation artifact denote the transformations in both directions (either by construction or through calculation), avoiding the cumbersome and error-prone task of manually writing and maintaining two coherent transformations.
Macedo N.  2010.  Translating Alloy specifications to the point-free style. Abstractnunomacedomsc.pdf

Every program starts from a model, an abstraction, which is iteratively re ned until we reach the
nal result, the implementation. However, at the end, one must ask: does the nal program resemble
in anyway the original model? Was the original idea correct to begin with? Formal methods
guarantee that those questions are answered positively, resorting to mathematical techniques. In
particular, in this thesis we are interested on the second factor: veri cation of formal models.
A trend of formal methods defends that they should be lightweight, resulting in a reduced
complexity of the speci cation, and automated analysis. Alloy was proposed as a solution for this
problem. In Alloy, the structures are described using a simple mathematical notation: relational
logic. A tool for model checking, automatic veri cation within a given scope, is also provided.
However, sometimes model checking is not enough and the need arises to perform unbounded
veri cations. The only way to do this is to mathematically prove that the speci cations are correct.
As such, there is the need to nd a mathematical logic expressive enough to be able to represent
the speci cations, while still being su ciently understandable.
We see the point-free style, a style where there are no variables or quanti cations, as a kind
of Laplace transform, where complex problems are made simple. Being Alloy completely relational,
we believe that a point-free relational logic is the natural framework to reason about Alloy
speci cations.
Our goal is to present a translation from Alloy speci cations to a point-free relational calculus,
which can then be mathematically proven, either resorting to proof assistants or to manual proving.
Since our motivation for the use of point-free is simplicity, we will focus on obtaining expressions
that are simple enough for manipulation and proofs about them.