Stack操作部分的形式约束 Initialise的前 后置断言 initialise(s) pre true (none * post elems'={} (elems'is an empty set * push(s,a) pre :lelemsl<max (s is not full * post c'>c and (a,c)Eelems' (the new time-stamp c'is larger than the previous time-stamp c'and the pair (a,c)belong to S*) push的前后 置断言Stack操作部分的形式约束 Initialise的前 后置断言 push的前后 置断言