tractable object models Daniel Jackson Software Design Group MIT Laboratory for Computer Science WG 2.9 ∑ Flims ∑ February 7, 2000

lightweight formal methods


semantic minimalism

relational structure


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


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