Taking modeling seriously: A hands-on approach to Alloy

Description
The modeling of humanities data is a core activity (some say the core activity) of the digital humanities. The activity so described may take a wide variety of forms; often the term is used for any compact description of a domain, whether in prose or in user-interface metaphors. Machine-processable descriptions are probably more common, but these, too, vary: the definition of an XML vocabulary, the table declarations for a SQL database, the data structures or even the executable code of a program may all be described informally as offering a ‘model’ of some domain or other.
The term model, however, is here applied more narrowly to expressions in some well defined formalization. Models are most useful when formalized in a declarative not a procedural notation and when their logical import is clear. Formulating precise models can be difficult. Inconsistencies and unforeseen interferences between parts of the model can easily creep in. With informal definitions, such shortcomings can remain undetected for long periods, even until after the model has been put to use. Formally defined models, on the other hand, can be tested systematically for logical consistency; their consequences can be established systematically. Such testing can help uncover shortcomings in a timely manner.
Alloy is a tool for “lightweight formal methods”, which makes it easier to test the implications of models and to check assumptions for plausibility, consistency, and completeness. Its usual application area is the testing of software designs but the variant of first-order logic provided by Alloy is by no means limited to the description of software or electronic objects. It has been successfully used to formalize notions far removed from any software, including the nature of transcription, an application of the type/token distinction to document structure, and fragments of Goodman and Nelson's mereology and of Hilbert's formulation of Euclidean geometry. Alloy's logic is powerful enough to formulate interesting concepts, while remaining weak enough to be tractable for machine processing. Using Alloy's syntax, a modeler can formulate the axioms of a model and augment them by asserting that certain properties hold for all instances of the model, or by defining predicates which characterize particular instances of the model. The Alloy Analyzer can test the assertions and illustrate the predicates, by seeking counter-examples to the assertion or instances of the predicate.
This one-day tutorial introduces digital humanists to the use of Alloy for modeling. Topics include:
• introduction to Alloy's logic
• compressed summary of Alloy syntax
• use of Alloy for formulating assertions and predicates
• describing individual test cases for Alloy
• Alloy's place in the larger context and Alloy's relation to light-weight formal methods, to other formal methods (e.g. Z), and to theorem-provers
• limits on Alloy's logic, from a theoretical point of view (how Alloy and other tools deal with Goedel's incompleteness result and Turing's halting problem), and from a practical point of view (modeling recursion using transitive closure)
Examples will be drawn from domains discussed at recent DH conferences.
Prerequisites: some prior exposure to symbolic logic and/or programming is probably desirable; failing that, highly motivated participants may be able to benefit from the workshop if they have sufficiently high tolerance for exposure to new material.
Participants should bring a laptop computer with a current installation of Java; they may optionally preinstall Alloy 4.2 or they may install it during the workshop.
Target audience and expected number of participants
Short answer: not a large target audience (but a choice one!); estimated attendance perhaps 5-10 (no evidence).
The target audience consists of digital humanists interested in techniques for formalizing important concepts and tools for working with such formalizations. The tutorial deals with high level data modeling concepts. Some prior exposure to symbolic logic and/or programming is desirable; failing that, highly motivated participants may be able to benefit from the workshop if they have sufficiently high tolerance for exposure to new material. Participants should bring a laptop computer with a current installation of Java; they may optionally pre- install Alloy 4.2 or they may install it during the workshop.
Outline
Full-day outline
I'd prefer to teach this as a full-day tutorial; that allows time for a mixture of lecture-style presentation of information and hands-on exercises. A tentative full-day schedule is:
9:00-10:30 Introduction to the course
• Modeling, formal logic, formal methods. Lightweight formal methods; Alloy.
• Demonstration: Alloy model of a Web interface (capabilities, security issues, user information).
• Demonstration: Using Alloy to generate test cases.
• The small-scope hypothesis; how Alloy manages to be useful despite Goedel's Theorem.
• Hands-on exercise: Using the Alloy Analyzer.
10:30-11:00 Break
11:00-12:30 Alloy's first-order logic
• Atoms, relations, tuples, sets. Basics of syntax: signatures, relations, multiplicities.
• Hands-on exercise(s) (logic puzzles, simple proofs from logic textbooks).
• Styles of expression: predicate-calculus style, navigational style, relational style. More syntax: assertions, predicates, quantification, let-expressions.
• Using Alloy to model concepts: FRBR entities, metadata records, XML and non-XML document structures.
• More exercises(s).
12:30-2:00 Lunch
2:00-3:30 Alloy as a tool for software design
• Examples: using Alloy to model an interactive concordance system, a query interface, a database system.
• Hands-on exercises.
• Idioms for modeling state, change, and dynamic systems in Alloy.
• Idioms for testing specific instances with Alloy.
3:30-4:00 Break
4:00-5:30 Recursion, Conclusion
• Using transitive closure to model recursion.
• Hands-on exercises.
• Review, questions, clarifications.
• Where to go from here? Further Alloy resources, other tools for formal methods and theorem proving.