Stack操作部分的形式约束 empty(s) pre true post empty(s)=(l elemsl =0) full(s) pre true post full(s)=(l elemsl max) 这些数据规约和操作规约明确了这个数据结构的： 成员数据类型、组织方式、使用方式 但这些规约和具体的数据结构实现无关：数组方式？链表方式？ 实现这个ADT时：必须验证实现方法保持了这些约束的成立Stack操作部分的形式约束 这些数据规约和操作规约明确了这个数据结构的： 成员数据类型、组织方式、使用方式 但这些规约和具体的数据结构实现无关：数组方式？链表方式？ 实现这个ADT时：必须验证实现方法保持了这些约束的成立