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