#base: inv4(init,i) #inductive: istep4(i) #successor: s' #action: want(s,k) #constants: k : -> Pid #effective: pc(s,k) = l1 #case: i = k (i = k) = false #case: pc(s,i) = l2 (pc(s,i) = l2) = false #case: i \in queue(s) = true i \in queue(s) = false #action: try(s,k) #constants: k : -> Pid #effective: pc(s,k) = l2 top(queue(s)) = k #case: i = k (i = k) = false #action: exit(s,k) #constants: k : -> Pid l : -> Pid q : -> Queue #effective: pc(s,k) = cs #lemma: inv2(s,k) #case: i = k (i = k) = false #case: pc(s,i) = l2 (pc(s,i) = l2) = false #case: queue(s) = empty queue(s) = l q #case: l = k (l = k) = false #case: empty?(q) = true empty?(q) = false