An Institution for Alloy and Its Translation to Second-Order Logic

Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need for more sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic.

1. 1.

   To represent a tuple of \(n\) elements, \(v_1, \dots , v_n\), we use notations \((v_1, \dots , v_n)\) and \(v_1, \dots , v_n\) interchangeably, the latter being usually chosen if potential ambiguity is ruled out by the context.

2. 2.

   Full models at github.com/nevrenato/IRI_FMI_Annex.

This work is funded by ERDF—European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through FCT, the Portuguese Foundation for Science and Technology, within projects FCOMP-01-0124-FEDER-028923, project FCOMP-01-0124-FEDER-022690 and NORTE-01-0124-FEDER-000060.

Authors and Affiliations

1. INESC TEC (HASLab), University of Minho, Braga, Portugal

   Renato Neves & Luís Barbosa

2. Department of Mathematics, University of Aveiro, Aveiro, Portugal

   Alexandre Madeira

3. Center for Research and Development in Mathematics and Applications—Department of Mathematics, University of Aveiro, Aveiro, Portugal

   Manuel Martins

Corresponding authors

Correspondence to Renato Neves or Luís Barbosa .

Editors and Affiliations

1. Laboratoire de Communication dans les Systèmes Informatiques, Ecole Nationale Supérieure d’Informatique, Algiers, Algeria

   Thouraya Bouabana-Tebibel

2. SPAWAR Systems Center Pacific, San Diego, USA

   Stuart H. Rubin

Appendix A: Proofs

1.1 A.1 Lemma 1

The following commuting diagram of Alloy signature morphisms is a strong amalgamation square.

Proof.

Let \(M_1\) be an \((S,m,R,X + \{x\})\)–model, and \(M_2\) an \((S',m',R',X')\)–model, such that \(Mod^\mathcal {A}(x)(M_1) = Mod^\mathcal {A}(\varphi )(M_2)\). Thus, for any \(\pi \in S_t, M_{1\pi } = M_{2\varphi _{kd}(\pi )}\), for any \(\pi \in R_w, M_{1\pi } = M_{2\varphi _{rl}(\pi )}\), for any \(\pi \in X,\) \(M_{1\pi } = M_{2\varphi _{vr}(\pi )}\), and \(|M_1| = |M_2|\).

Then, let us define an \((S',m',R,',X' + \{x\})\)-model \(M'\) by stating that: For all \(\pi \in S'_t, M_{2\pi } = M'_{\pi }\); for all \(\pi \in R'_w, M'_{\pi } = M_{2\pi }\); for all \(\pi \in X', M_{2\pi } = M'_\pi \); \(|M_2| = |M'|\), and \(M_{1x} = M'_x\). Clearly, \(M_1 = Mod^\mathcal {A}(\varphi ')(M')\) and \(M_2 = Mod^\mathcal {A}(x^\varphi )(M')\). Also it is not difficult to show that \(M'\) is unique. Therefore the diagram above is a strong amalgamation square. \(\square \)

1.2 A.2 Lemma 2

For any signature morphism \(\varphi : \varSigma \rightarrow \varSigma '\) in \(Sign^\mathcal {A}\), any \(\varSigma \)–expression \(e\), and any \(\varSigma '\)–model \(M'\),

Proof.

Consider first the case \(e := \pi \), for \(\pi \in (R_\varSigma )_w\):

Proofs for when \(\pi \in (S_\varSigma )_{All}\) or \(\pi \in X_\varSigma \) are analogous.

When \(e := e + e'\):

Proofs for the remaining operators are analogous. \(\square \)

1.3 A.3 Lemma 3

The following commuting square of model morphisms and model transformations is a strong amalgamation square,

Proof.

Let \(M_1\) be an \((S,m,R,X + \{x\})\)–model and \(M_2\) a \((S',F',P')\)–model such that \(Mod^\mathcal {A}(x^\beta )(M_1) = \beta _{(S,m,R,X)}(M_2)\). I.e., for any \(\pi \in S_{All}\,\cup \, R_w \,\cup \, X\), \(M_{1\pi } = M_{2\pi }\) and \(|M_1|=|M_2|\).

Then let us define an \((S',F'+ \{x\},P')\)–model \(M'\) such that for any \(s \in S', |M'_s| = |M_{2s}|\); for any \(\sigma \in F'_w, M'_\sigma = M_{2\sigma }\); for any \(\pi \in P'_w, M'_\pi = M_{2\pi }\); \(M'_{x} = \{M_{1x}\}\). Clearly, we have \(M_1 = \beta _{(S,m,R,X+\{x\})}(M')\) and \(M_2 = Mod^{\textsc {SOL}^{pres}}(x)(M')\). Moreover, it is not difficult to show that \(M'\) is unique. Therefore the diagram above is a strong amalgamation square. \(\square \)

1.4 A.4 Lemma 4

Let \(\varSigma = (S_\varSigma ,m_\varSigma ,R_\varSigma ,X_\varSigma )\) be a signature in \(Sign^\mathcal {A}\), \(M'\) a \(\varPhi (\varSigma )\)-model \(M'\), and \(e\) a \(\varSigma \)-expression. Then, for any tuple \((v_1,\dots ,v_n) \in X_\varSigma \) with \(n = |e|\), we have

Proof.

When \(e := \pi , \pi \in (R_\varSigma )_w \cup (S_\varSigma )_{All}\):

When \(e := \pi , \pi \in X_\varSigma \):

When \(e := e \> .\> e'\):

When \(e :\)= ⌃\(e\):

When \(e := {\sim }e\):

When \(e := e + e'\):

Proofs for the remaining cases are analogous. \(\square \)

1.5 A.5 Theorem 2

The satisfaction condition holds in \((\varPhi ,\alpha ,\beta ) : \textsc {Alloy}\ \rightarrow \textsc {SOL}^{pres}\). I.e., given a signature \(\varSigma \in |Sign^\mathcal {A}|\), a \(\varPhi (\varSigma )\)-model \(M'\), and a \(\varSigma \)-sentence \(\rho \)

Proof.

When \(\rho := e \> \mathtt {in} \> e'\):

When \(\rho := \mathtt {not}\; \rho \):

For implication the proof is analogous

When \(\rho := ( \mathtt {all} \> x : e) \> \rho \):

\(\square \)

Reprints and permissions

© 2014 Springer International Publishing Switzerland

Policies and ethics