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).