How do constraints defined in Alloy result in better software?

Question

Alloy newbie here.

I really like creating constraints in Alloy and having the analyzer check that the model is valid per the constraints.

But I ask myself, “Are these constraint definitions mere mental gymnastics, or will they help build better software?”

Let’s take a specific example. In a model of an email client’s address book one might define this constraint for adding a new entry into the address book:

The address mapping in the new book b’ is equal to the address mapping in the old book b, with the addition of a link from the name to the address. This constraint is expressed in Alloy as: b'.addr = b.addr + n->a

That is beautiful.

But I am struggling to see its relevance when the add operation is implemented in code. For instance, I implemented the add operation in Common Lisp:

(defun add (b n a)
   "Add a new entry, (n a), to address book b"
   (adjoin (list n a) b :key #'first))

In words: “Here is a definition of a function named add which has three parameters: b, n, and a (book, name, address). Use the Common Lisp set function, adjoin, to add the list (n a) to b.”

That function seems to correctly implement a simple add function. What do I do with the constraint that I defined in Alloy? Should I write additional code that expresses the constraint? In pseudo-code: [1]

(defun add (b n a)
   "Add a new entry, (n a), to address book b"
   (adjoin (list n a) b :key #'first)
   Check that nothing has changed in the
   address book except that it now has
   a n->a mapping)

Writing such code seems like a lot of work, with no apparent benefit.

So my question is this: When implementing an Alloy model in code, what should I do with the constraints that are defined in Alloy?

Also, is there a tutorial which describes how to convert Alloy models to code, including a description of how Alloy constraint definitions are used in code?

Thank you.

[1] Note: I realize that there is a language extension called Screamer for constraint programming in Common Lisp

Answer 1

I believe the question stems from a minor misunderstanding of the goals and capabilities of some of the modeling languages like Alloy and touches some of the fundamental aspects of formal methods, verification and software modeling. Probably good resources to get a background story that would make things more clear include books like Calculus of Computation, as well as the book about Alloy you've mentioned.

Constraints are first-class citizens of the Alloy modeling language. The idea is that constraints reflect the semantics of the code one wants to model (and check properties about). Thus, from one perspective, Alloy program represents the code itself and there is no need for writing additional code (e.g. in a functional language) or mixing declared constraints with code. However, Alloy programs cannot be directly executed; rather, they can only be used to produce models according to such programs (i.e. sets of constraints).

More specifically, the Alloy constraint b'.addr = b.addr + n->a, might, under an appropriate interpretation, indeed capture the behavior of the add operation in Lisp, so that checking some properties that involve the constraint corresponds to checking whether those properties hold for the given operation in Lisp. This is the standard (and, arguably, intended) use of Alloy for modeling and verification of software. (In addition, Alloy is frequently used to model systems that don't have clear mappings into programs, like certain kinds of cyber-physical systems [1].) Note that this of course entails that the model one writes in Alloy must correctly model the program at hand (with respects to its semantics), in order for the checking of properties to make sense.

As mentioned, Alloy itself cannot produce executable code (such as the one you've given, written in Common Lisp). However, there are multiple approaches that use Alloy and models that Alloy generates to produce fragments of code or test cases. (Again, according to the specific program at hand.) In addition, an extension of Alloy, called Alloy* [2], which adds the possibility of solving higher order constraints within Alloy (quantification over relations) can be used to generate programs; actual code that performs the operation and accepts different inputs (similarly to the add function, according to the model). Again, such programs are represented with Alloy models and one needs to (perform additional effort to) translate those models into programs in some desired programming language.

Having that said, note that some (verification) systems indeed allow you to mix specifications with code, where specifications might be: written in the same way as the code that is to be executed (like in the verification/synthesis framework Leon [3]); or written in a distinct language (from the language of executable code), while the specifications are bound to code by some other means (like annotations in Dafny [4]).

[1] Kang, Eunsuk, et al. "Model-based security analysis of a water treatment system." Proceedings of the 2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems. ACM, 2016.

[2] Milicevic, Aleksandar, et al. "Alloy*: A general-purpose higher-order relational constraint solver." Proceedings of the 37th International Conference on Software Engineering-Volume 1. IEEE Press, 2015.

[3] Blanc, Régis, et al. "An overview of the Leon verification system: Verification by translation to recursive functions." Proceedings of the 4th Workshop on Scala. ACM, 2013.

[4] Leino, K. Rustan M. "Dafny: An automatic program verifier for functional correctness." International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer Berlin Heidelberg, 2010.