A hands-on introduction to Alloy
Lincoln, Nebraska
15 July 2013
This full-day hands-on tutorial introduces Alloy as a modeling
tool for digital humanities work.
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.
Properly speaking, however, the term model is most usefully applied 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 our models and check our
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 can be (and 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.
Hands-on exercises will give students experience actually writing
simple models in Alloy and examining their properties using the
Alloy Analyzer.
Participants should have good knowledge of XML syntax;
knowledge of XPath and XSLT (1.0 or 2.0) will be helpful but is not a
prerequisite. Familiarity with basic programming concepts (input,
output, types, flow of control will be helpful (or alternatively, the
ability to confront new concepts without fear).
Topics and syllabus
Topics include:
-
Introduction
Modeling, formal logic, formal methods. Lightweight formal methods;
Alloy.
Demonstration: Alloy model of manuscript traditions.
Hands-on exercise. Using the Analyzer:
the absolute minimum of Alloy syntax (sig, fact,
pred, run, assert, check)
and a ‘hello, world’ example (Gen. 1:1).
-
Alloy's first-order logic
Alloy's universe of discourse (atoms, tuples, relations, sets).
Basic syntax: signatures, sub-signatures, subset signatures,
multiplicities, compound objects, relations.
The small-scope hypothesis; how Alloy manages to
be useful despite Goedel's Theorem.
Set operations; hands-on exercise.
Logical operators, sentential logic; hands-on exercise.
-
Quantification and relations
Universal and existential quantification; the keyword one
and Russell's definite descriptions; exercise.
Operations on relations; exercise.
Set comprehensions, let expressions; exercise.
More about the Analyzer: customizing the theme, exporting
examples; the evaluator.
Facts, predicates, assertions, functions.
Styles of expression: predicate-calculus style, navigational style,
relational style.
Using Alloy to model concepts: bibliographic entities in FRBR
(Functional Reqirements for Bibliographic Records).
-
Recursion, conclusion
Recursion via transitive closure; serial-adder example.
Dynamic systems: operations, traces, events.
Q/A and pointers for further information.
Resources
Some materials of possible interest:
Prerequisites
There are no formal prerequisites. Some prior exposure to symbolic
logic and/or programming is probably desirable; failing that,
sufficiently motivated participants may be able to benefit from the
workshop if they have sufficiently high tolerance for exposure to new
material.
Students 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.
Logistics
When and where
This course will be held from 9:30 a.m. to 5:30 p.m.
Monday, 15 July 2013,
in conjunction with the
Digital Humanites 2013
conference hosted by the University of Nebraska - Lincoln.
Thanks to the conference sponsors for hosting the tutorial.
Who
Michael Sperberg-McQueen
is the founder of Black Mesa Technologies.
He has served as co-editor of the XML 1.0 specification, the
Text Encoding Initiative's
Guidelines for Text Encoding and Interchange,
and the XML Schema Definition Language (XSD) 1.1 specification;
in 2003 he was awarded the XML Cup for contributions to the
development and spread of XML.