sample specs
sample properties
assert NoNullDerefs {Merge -> Null !in Derefs’}
assert NoLoss {Merge -> result.*next = p.*next + q.*next}
assert NoCycles {Merge && Acyclic (p) && Acyclic (q) -> Acyclic (result)}
counterexample to NoCycles
p = O1
q = O1
next = {O1 -> O0}
…
result = O1
next’ = {O1 -> O1}