Stack操作部分的形式约束 pop(s) pre l elemsl>0 (s is not empty * post :3(a,b)E elems such that ((a,b)is the element in s with largest [v(p,q)∈elems b≥ql time-stamp b and is deleted from and elems'=elems-{(a,b)} elems * top(s) pre lelemsl>0 post :3(a,b)E elems such that (*(a,b)is the element in S with [v(p,q)∈elems b≥q] largest time-stamp b and a is and top(s)=a returned as the value of the function.Note that c and s are not changed *Stack操作部分的形式约束