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

#relations

scope

5

10

15

20

3

6

9

12

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

note
• in is both ? and ?

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

sets
s : T m s has m elements

relations
r : S m -> T n r maps each S to n T’s

r maps m S’s to each T

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

model COM {

domain {Component, Interface, IID}

state {

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

model COM {

domain {Component, {c0} Interface, {i0, i1} IID} {x0,x1}

state {

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

‘proofs’

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

with Mandana Vaziri

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)

with Sarfraz Khurshid

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

fixed in new version

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