Submission to SEFM'11 Special Issue

This is an extended version of our paper "Translating Alloy
Specifications to UML Class Diagrams Annotated with OCL" accepted at
SEFM'11. We believe this version includes more that the required 25%
new material. Here is a detailed list of the new contributions:

- We allow both mutable and immutable fields. Mutable ones must
  have the Time column, while immutable don't. Immutable sets are
  captured by signature inclusion. Immutable fields are translated to
  properties (either associations or atributes) with the readOnly
  attribute.

- We translate enum signature declarations to enumeration classes.

- Since OCL 2.3 now implements a closure operator, we can translate
  arbitrary closures of relational expressions.

- We also implemented the translation of integer expression #R for
  expressions R of arbitrary arity.

- We allow a more flexible Alloy syntax, namely checking the
  multiplicity of a relation, quantifying over expressions,
  and comprehension over expressions.

- We extended the address book example to cover some of the new
  features.

- We characterized formally the (safe) OCL subset generated/accepted
  by our translation.

- We developed an OCL to Alloy translation that, unlike previously
  existing ones, handles correctly pre- and post-conditions by
  translating to the local state idiom. It also supports closures.

- We developed a new roundtrip case study, where we start with an
  UML+OCL specification, translate to Alloy, refine the model, and
  translate back to UML+OCL.

- We implemented all the new features in a open source toolset
  available for download at http://sourceforge.net/projects/alloymda/
  together with additional examples.

We also improved the text all over, including the following
clarifications:

- Explained the Alloy examples with a bit more detail.

- We detailed a bit more some issues that may occur related to Alloy
  type system, namely clarified how to handle remainder atomic
  signatures that occur when a non-abstract signature is extended.

- We clarified the need for explicit type checking and type casts in
  some expressions, and how exactly that problem can be solved.

Best regards,
Alcino Cunha