a relational logic, its analysis & application Daniel Jackson, MIT WG 2.3 · Newcastle April 4, 2000
motivations
progress
acknowledgments
overview
first-order relational logic
examples
full model (1)
full model (2)
kernel: type decls
kernel: formulas
kernel: expressions
semantics: formulas
semantics: expressions
full language
declaration shorthands
COM basics
alloy model
an instance
rules
aggregation
results
how alcoa helped
how alcoa helped (2)
proving NoHiding
performance
other applications: code
other applications: algorithms
language implications
conclusions