open util/boolean sig E {} // generic type parameter sig Array { length: Int, data: {i: Int | 0 =< i && i < length} -> lone E } { length >= 0 } pred show{ some l: List | l.rep.shared = False some l: List | l.rep.shared = True some disj l1, l2: List | l1.rep = l2.rep } run show for 3 but exactly 2 Array, exactly 3 E, 3 int sig ListRep { elems: Array, // inv1: elems is non-null shared: Bool } // inv 2: elems is not shared (from ListReps) fact inv2 { all disj lr1, lr2: ListRep | lr1.elems != lr2.elems } sig Object{} sig List extends Object { rep: ListRep, // inv6: rep is non-null len: Int } { 0 <= len && len <= rep.elems.length // inv. 7 : 0 <= len <= rep.elem } // inv7 can also be expressed like this: /* fact inv7{ all l: List | 0 <= l.len and l.len =< l.rep.elems.length } */ // inv4: if shared is false, then list rep object represents at most one list object // (same as if two list reps are accessed by one list, the shared bit needs to be true) fact inv4 { all disj l1, l2: List | l1.rep = l2.rep => l1.rep.shared = True } assert inv4{ all l1: List | l1.rep.shared = False => no l2: List | l2 != l1 and l2.rep = l1.rep } check inv4 for 7