tractable object modelsDaniel JacksonSoftware Design GroupMIT Laboratory for Computer ScienceWG 2.9 · Flims · February 7, 2000

lightweight formal methods

progress

semantic minimalism

relational structure

example

modelling implication

partial function problem

my approach

an example

basic notions

object model diagram

Alloy model: declarations

an indicative invariant

a safety condition

two definitions

policy invariants

an operation

analysis strategy

bug example, inconsistency

bug example, implication

output

bug example, preservation of invariant

funky overlap

why it’s hard (1)

small scope hypothesis

why it’s hard (2)

translating to SAT

research status

conclusion