Concurrent object O Client code c void push(int v)I int po push (7) local b: =false x, t; push (6) X:=new Node(v) x= popo While op: x, next = t b= cas(&top, t, x); Whole program C[OJ How to specify/prove correctness?Whole program C[O] … push(7); x = pop(); … … push(6); … Client code C Concurrent object O void push(int v) { local b:=false, x, t; x := new Node(v); while (!b) { t := top; x.next = t; b = cas(&top, t, x); } } … int pop() { … … } How to specify/prove correctness?