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