type List = {bool value; data next:List; bool free;} data freenodes:List; proc insert(data x:List, pointer p:List, bool v):void [(xp | x=null & p=null) & freenodes!=null & allpos t of List: freenodest <=> t.free=true] { pointer q:List; if (p!=null) { if (p.next=null) { q = x.next; p = freenodes; freenodes.free = false; freenodes = freenodes.next; x.next = p; } else { q = p.next; p.next = freenodes; freenodes.free = false; freenodes = freenodes.next; p = p.next; } } else { q = null; p = freenodes; freenodes.free = false; freenodes = freenodes.next; x = p; } p.next = q; p.value = v; } [allpos t of List: freenodest <=> t.free=true]