a small experiment
subject
8 sample list procedures from [Dor, Rodeh, Sagiv 99]
merge, delete, search, reverse, etc
translated by hand into Alloy
properties checked
no null derefs, result not null
no cycles created
set inclusions (eg, for delete, merge)
results
found bugs identified by [DRS99] and one more
for scope of 3, 2 unrollings: a few secs, except for merge