a relational logic, its analysis & applicationDaniel Jackson, MITWG 2.3 · NewcastleApril 4, 2000
motivations
lightweight formal methods
- small models, focusing on risky bits
- incremental construction (so declarative)
- fast, automatic tools
executability without loss of abstraction
two sources of complexity, two styles of model
- interleaving, local machines
- state structure, global machine
progress
nitpick (1996)
- sets & binary relations
- Z-like schema calculus
alcoa (1999)
- first-order quantifiers
- object model declarations
- mutability constraints
alcoa’ (2000)
- structures (hierarchy)
- sequential composition
- numbers, sequences & orders
acknowledgments
thanks to …
- Doug Ross, for funding this work
- Jim Horning, ‘Formal Spec as a Design Tool’
- Ken McMillan, SMV
- Greg Nelson, for suggesting DP
overview
language
- relational ops, esp. navigation
- scalars as sets
- structuring for checking
an application (with Kevin Sullivan)
- Microsoft COM
- simplifying with Alcoa
analysis method (with Ilya Shlyakhter)
- reduction to SAT
- exploiting symmetry
first-order relational logic
predicate logic relational logic
all x | S(x) -> (T(x) || U(x)) S in (T + U)
all x, y | S(x) && R(x,y) -> T(y) S.R in T
all x | some y | loves (y, x) all x | some y | x in y.loves
can’t express no x | x in x.+R
examples
“One man’s ceiling is another man’s floor” (Paul Simon, 1973)
ceiling, floor : Man -> Platform!
all m: Man | some n: Man - m | m.ceiling = n.floor
“Everybody loves my baby, but my baby loves only me” (?)
baby, me : Person!
loves : Person -> Person
all p | baby in p.loves
baby.loves = me
full model (1)
model CeilingsAndFloors {
domain { Man, Platform }
state { ceiling, floor : Man -> Platform! }
// one man’s ceiling is another man’s floor
inv { all m: Man | some n: Man - m | m.ceiling = n.floor }
// one man’s floor is another man’s ceiling
assert { all m: Man | some n: Man - m | m.floor = n.ceiling }
}
full model (2)
model Baby {domain {Person}state { me, baby : Person! loves : Person -> Person }inv { all p | baby in p.loves baby.loves = me }assert {me = baby}}
kernel: type decls
grammar
problem ::= decl* formula
decl ::= var : typexpr
typexpr ::= type | type -> type | type => typexpr
declarations
s : T s is a set of atoms drawn from basic type T
r : T -> U r is a relation from T to U
f : T => t f is a function from each atom in T to value of type t
note
- scalars are just singleton sets
- functions are still first-order
kernel: formulas
grammar
formula ::=expr in expr subset| ! formula negation| formula && formula conjunction| formula || formula disjunction| all v : type | formula universal| some v : type | formula existential
kernel: expressions
grammar
expr ::= | expr + expr union| expr & expr intersection| expr - expr difference| expr . expr navigation| expr [var] application| ~ expr transpose | + expr transitive closure| {v : t | formula} comprehension| var
note
- e.p is relational image of e under p
semantics: formulas
M : formula ? env ? boolean
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
M [a in b] e = X[a]e ? X[b]e
M [! F] e = ? M[F]e
M [F && G] e = M[F]e ? M[G]e
M [all v: t | F] e = ? {M[F] (e ? v ? x) | x ? e(t)}
semantics: expressions
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
X [a + b] e = X[a]e ? X[b]e
X [a . b] e = {y | ?x. x ? X[a]e ? (x,y) ? X[b]e}
X [~a] e = {(x,y) | (y,x) ? X[a]e}
X [+a] e = the smallest r such that r ; r ? x ? X[a]e ? x
X [{v: t | F}] e = {x ? e(t) | M[F] (e ? v ? x)}
X [v] e = e(v)
X [a[v]] e = e(a)(v)
full language
domains
domain {s} declares s : _s
quantifier shorthands
sole v: t | f short for some v: t | {w: t | f} in v
all x | f short for all x : s | f where s is inferred domain
Q e short for Q v | v in e
paragraphs
inv invariant (implicitly imported)
def definition (implicitly imported)
cond condition (invocable)
op operation (imports inv and inv’)
assert assertion (negated)
declaration shorthands
multiplicity symbols
+ one or more
? zero or one
! exactly one
relations
r : S m -> T n r maps each S to n T’s
me : Person!
Merlin : Person?
friends : Person-> Person
mum : Person+ -> Mother!
wife :Person? -> Person? (C)
Person! -> Person! (J)
Person? -> Person (I)
COM basics
basic notions
- components offer interfaces
- each interface has types (IIDs)
- dynamic negotiation by query
standard rules
- chat & code fragments [Box99]
- modelled in Z [Sullivan99]
- eg, query on IID_Unknown gives identity interface
alloy model
domain {Component, Interface, IID}
interfaces : Component + -> Interface
iids, iids_known : Interface -> IID+
qi : Interface => IID -> Interface?
reaches: Interface -> Interface
def reaches {all i | i.reaches = IID.qi[i]}
def iids_known {all i | i.iids_known = {x | some x.qi[i]}}
an instance
domain {Component, {c0} Interface, {i0, i1} IID} {x0,x1}
interfaces : Component + -> Interface {(c0,i0), (c0,i1)}
iids : Interface -> IID+ {(i0,x0), (i1,x1)}
iids_known : Interface -> IID+ {(i0,x0), (i0,x1), (i1,x1)}
qi : Interface => IID -> Interface? {(i0, {(x0,i0),(x1,i1)}),…}
reaches: Interface -> Interface {(i0,i1), (i1,i0)}
def reaches {all i | i.reaches = IID.qi[i]}
def iids_known {all i | i.iids_known = {x | some x.qi[i]}}
rules
inv QueriesSound {all i | all x: i.iids_known | x in x.qi[i].iids}inv QueriesLocal {all c | all j : c.interfaces | all x: IID | x.qi[j] in c.interfaces}
inv Identity {some Unknown | all c | some j: c.interfaces | all i: c.interfaces | j = Unknown.qi[i]}
inv Reflexivity {all i | i.iids in i.iids_known}
inv Symmetry {all i, j | j in i.reaches -> i.iids in j.iids_known}
inv Transitivity {all i, j | j in i.reaches -> j.iids_known in i.iids_known}
aggregation
motivation
- compose components
- avoid cost of delegation
- so share interfaces
what Sullivan discovered
- can’t hide inner interfaces!
assert NoHiding {
all c, d | some (c.interfaces & d.interfaces) -> c.interfaces.iids = d.interfaces.iids }
results
results
- simplified model
to ~70% in Z->Alloy
to ~50% reformulating
- checks of Sullivan’s theorems
- checks of other speculations
useful?
- basis for exploration
- succinct & precise explanation
- helps rewrite informal rules
how alcoa helped
checking consistency
- show me double aggregation
checking assertions
- can new rule replace Ref, Sym, Trans?
“every interface of a component knows all its IIDs”
checking reformulations
- can we remove notion of identity interface?
- are theorems still true for weaker rules?
comparing versions
- is new version of transitivity same as old one?
how alcoa helped (2)
finding proofs
- which premises are needed?
- check assertion with each on/off
example
- NoHiding doesn’t need Reflexivity or Transitivity
- helps find the proof (which axioms to use?)
- helps check the proof (used all axioms?)
proving NoHiding
- need
ID: identity query gives one interface for a component
SYM: if i reaches j, then j knows the IID’s of i
LOCAL: queries don’t cross components
SOUND: query results in interface with requested IID
- proof
suppose c and d share interface i, and c has another interface j
by ID, identity query on i yields (another) shared interface id
by ID, query for identity on j yields id
by SYM, id knows IIDs of j
by LOCAL, query for an IID x of j on id yields interface k of d
by SOUND, k has IID x
so x is an IID of d
performance
counterexamples
- all s
- none require scope ɯ
Scope 2 3 4 5 6Space (bits) 54 123 228 375 570Proof (secs) 2s 2-3s 3-40s 5-609s 7-7580s
other applications: code
scheme
- translate Java procedure to Alloy formula
- check pre && code -> post
examples
- suite of list procedures
all known anomalies (plus one) caught with one loop unrolling
set properties checked (eg, merge forms union)
ordering properties checked (eg, merge preserves order)
- now working on global invariants in CTAS
other applications: algorithms
intentional naming [Balakrishnan et al, SOSP 99]
- scheme for locating resources by specs
- query, database: trees of alternating attribute/value pairs
- algorithm for lookup
what we did
- translated pseudocode to Alloy, peeped at code
- 1400+1900 loc, 50+30 lines of Alloy
- three kinds of check
basic properties (3)
properties of any naming scheme (3)
claims of paper (2)
language implications
first order restriction
- no liveness (eg, asserts about pre)
- spec by minimization tricky
- no sequential comp: needs 2d-order quantifier & structures
- no numbers or sequences
small (?) syntactic issues
- ascii, scalars as sets, object-model decls
specialized paragraphs
- different semantics (can turn off invariants)
- special checks (def is deterministic)
- can’t import invariants and compare them
conclusions
compromises
- partial models
- finite scope checking (but not spec)
- no temporal properties
- scale
200 bits: easy, seconds
1000 bits: sometimes easy (UML)
non-compromises
- partial models
- executable and abstract