1module examples/systems/views
2
3/*
4 * Model of views in object-oriented programming.
5 *
6 * Two object references, called the view and the backing,
7 * are related by a view mechanism when changes to the
8 * backing are automatically propagated to the view. Note
9 * that the state of a view need not be a projection of the
10 * state of the backing; the keySet method of Map, for
11 * example, produces two view relationships, and for the
12 * one in which the map is modified by changes to the key
13 * set, the value of the new map cannot be determined from
14 * the key set. Note that in the iterator view mechanism,
15 * the iterator is by this definition the backing object,
16 * since changes are propagated from iterator to collection
17 * and not vice versa. Oddly, a reference may be a view of
18 * more than one backing: there can be two iterators on the
19 * same collection, eg. A reference cannot be a view under
20 * more than one view type.
21 *
22 * A reference is made dirty when it is a backing for a view
23 * with which it is no longer related by the view invariant.
24 * This usually happens when a view is modified, either
25 * directly or via another backing. For example, changing a
26 * collection directly when it has an iterator invalidates
27 * it, as does changing the collection through one iterator
28 * when there are others.
29 *
30 * More work is needed if we want to model more closely the
31 * failure of an iterator when its collection is invalidated.
32 *
33 * As a terminological convention, when there are two
34 * complementary view relationships, we will give them types
35 * t and t'. For example, KeySetView propagates from map to
36 * set, and KeySetView' propagates from set to map.
37 *
38 * author: Daniel Jackson
39 */
40
41open util/ordering[State] as so
42open util/relation as rel
43
44sig Ref {}
45sig Object {}
46
47-- t->b->v in views when v is view of type t of backing b
48-- dirty contains refs that have been invalidated
49sig State {
50  refs: set Ref,
51  obj: refs -> one Object,
52  views: ViewType -> refs -> refs,
53  dirty: set refs
54--  , anyviews: Ref -> Ref -- for visualization
55  }
56-- {anyviews = ViewType.views}
57
58sig Map extends Object {
59  keys: set Ref,
60  map: keys -> one Ref
61  }{all s: State |  keys + Ref.map in s.refs}
62sig MapRef extends Ref {}
63fact {State.obj[MapRef] in Map}
64
65sig Iterator extends Object {
66  left, done: set Ref,
67  lastRef: lone done
68  }{all s: State | done + left + lastRef in s.refs}
69sig IteratorRef extends Ref {}
70fact {State.obj[IteratorRef] in Iterator}
71
72sig Set extends Object {
73  elts: set Ref
74  }{all s: State | elts in s.refs}
75sig SetRef extends Ref {}
76fact {State.obj[SetRef] in Set}
77
78abstract sig ViewType {}
79one sig KeySetView, KeySetView', IteratorView extends ViewType {}
80fact ViewTypes {
81  State.views[KeySetView] in MapRef -> SetRef
82  State.views[KeySetView'] in SetRef -> MapRef
83  State.views[IteratorView] in IteratorRef -> SetRef
84  all s: State | s.views[KeySetView] = ~(s.views[KeySetView'])
85  }
86
87/**
88 * mods is refs modified directly or by view mechanism
89 * doesn't handle possibility of modifying an object and its view at once?
90 * should we limit frame conds to non-dirty refs?
91 */
92pred modifies [pre, post: State, rs: set Ref] {
93  let vr = pre.views[ViewType], mods = rs.*vr {
94    all r: pre.refs - mods | pre.obj[r] = post.obj[r]
95    all b: mods, v: pre.refs, t: ViewType |
96      b->v in pre.views[t] => viewFrame [t, pre.obj[v], post.obj[v], post.obj[b]]
97    post.dirty = pre.dirty +
98      {b: pre.refs | some v: Ref, t: ViewType |
99          b->v in pre.views[t] && !viewFrame [t, pre.obj[v], post.obj[v], post.obj[b]]
100      }
101    }
102  }
103
104pred allocates [pre, post: State, rs: set Ref] {
105  no rs & pre.refs
106  post.refs = pre.refs + rs
107  }
108
109/**
110 * models frame condition that limits change to view object from v to v' when backing object changes to b'
111 */
112pred viewFrame [t: ViewType, v, v', b': Object] {
113  t in KeySetView => v'.elts = dom [b'.map]
114  t in KeySetView' => b'.elts = dom [v'.map]
115  t in KeySetView' => (b'.elts) <: (v.map) = (b'.elts) <: (v'.map)
116  t in IteratorView => v'.elts = b'.left + b'.done
117  }
118
119pred MapRef.keySet [pre, post: State, setRefs: SetRef] {
120  post.obj[setRefs].elts = dom [pre.obj[this].map]
121  modifies [pre, post, none]
122  allocates [pre, post, setRefs]
123  post.views = pre.views + KeySetView->this->setRefs + KeySetView'->setRefs->this
124  }
125
126pred MapRef.put [pre, post: State, k, v: Ref] {
127  post.obj[this].map = pre.obj[this].map ++ k->v
128  modifies [pre, post, this]
129  allocates [pre, post, none]
130  post.views = pre.views
131  }
132
133pred SetRef.iterator [pre, post: State, iterRef: IteratorRef] {
134  let i = post.obj[iterRef] {
135    i.left = pre.obj[this].elts
136    no i.done + i.lastRef
137    }
138  modifies [pre,post,none]
139  allocates [pre, post, iterRef]
140  post.views = pre.views + IteratorView->iterRef->this
141  }
142
143pred IteratorRef.remove [pre, post: State] {
144  let i = pre.obj[this], i' = post.obj[this] {
145    i'.left = i.left
146    i'.done = i.done - i.lastRef
147    no i'.lastRef
148    }
149  modifies [pre,post,this]
150  allocates [pre, post, none]
151  pre.views = post.views
152  }
153
154pred IteratorRef.next [pre, post: State, ref: Ref] {
155  let i = pre.obj[this], i' = post.obj[this] {
156    ref in i.left
157    i'.left = i.left - ref
158    i'.done = i.done + ref
159    i'.lastRef = ref
160    }
161  modifies [pre, post, this]
162  allocates [pre, post, none]
163  pre.views = post.views
164  }
165
166pred IteratorRef.hasNext [s: State] {
167  some s.obj[this].left
168  }
169
170assert zippishOK {
171  all
172    ks, vs: SetRef,
173    m: MapRef,
174    ki, vi: IteratorRef,
175    k, v: Ref |
176    let s0=so/first,
177    s1=so/next[s0],
178    s2=so/next[s1],
179    s3=so/next[s2],
180    s4=so/next[s3],
181    s5=so/next[s4],
182    s6=so/next[s5],
183    s7=so/next[s6] |
184  ({
185    precondition [s0, ks, vs, m]
186    no s0.dirty
187    ks.iterator [s0, s1, ki]
188    vs.iterator [s1, s2, vi]
189    ki.hasNext [s2]
190    vi.hasNext [s2]
191    ki.this/next [s2, s3, k]
192    vi.this/next [s3, s4, v]
193    m.put [s4, s5, k, v]
194    ki.remove [s5, s6]
195    vi.remove [s6, s7]
196  } => no State.dirty)
197  }
198
199pred precondition [pre: State, ks, vs, m: Ref] {
200  // all these conditions and other errors discovered in scope of 6 but 8,3
201  // in initial state, must have view invariants hold
202  (all t: ViewType, b, v: pre.refs |
203    b->v in pre.views[t] => viewFrame [t, pre.obj[v], pre.obj[v], pre.obj[b]])
204  // sets are not aliases
205--  ks != vs
206  // sets are not views of map
207--  no (ks+vs)->m & ViewType.pre.views
208  // no iterator currently on either set
209--  no Ref->(ks+vs) & ViewType.pre.views
210  }
211
212check zippishOK for 6 but 8 State, 3 ViewType expect 1
213
214/**
215 * experiment with controlling heap size
216 */
217fact {all s: State | #s.obj < 5}
218