ADT stack:set of elements of type elemtype (elemtype is used to refer to the type of the individual elements in a stack. Elemtype can potentially be any defined type * Stack-ADT Operations: procedure initialise(var S:stack); This procedure assigns an empty stack to S. ·定义栈的管理动作： procedure push(var S:stack;a:elemtype); Stack S should not be full.This procedure adds the element a at ·initialize(S):创建一个栈； the top of the stack. ·push(S,c:将c压入栈S中： procedure pop(var S:stack); Stack S should not be empty.The top element of the stack is ·top(S):栈顶元素； removed. ·pop(S):将栈顶元素去除； function top(S:stack):elemtype; ·empty(S):判定S是否为空 Stack S should be non-empty and this function returns the top element of the stack S.The stack S is left unchanged.(If elem- ·ful(s:判断S是否满 type is a structured type,this function should be rewritten as a procedure,see note 1 of section 3.1.) function empty(S:stack):boolean; This function returns true if S is empty and false otherwise. function full(S stack):boolean; If S is full this function returns a true value. Otherwise it returns a false value
Stack-ADT • 定义栈的管理动作： • initialize(S):创建一个栈； • push(S,c):将c压入栈S中; • top(S):栈顶元素； • pop(S):将栈顶元素去除; • empty(S):判定S是否为空 • full(s):判断S是否满
如果我们在构造自己的数据组织方式时，写出 了一个关于这个方式的“约定”，而暂时没有 涉及实现细节，甚至不再关心实现细节而交由 其他人员实现时，我们写出来的“约定”就有 了新名词： 抽象数据类型：ADT
如果我们在构造自己的数据组织方式时，写出 了一个关于这个方式的“约定”，而暂时没有 涉及实现细节，甚至不再关心实现细节而交由 其他人员实现时，我们写出来的“约定”就有 了新名词： 抽象数据类型：ADT
ADT stack:set of elements of type elemtype (elemtype is used to refer to the type of the individual elements in a stack. Elemtype can potentially be any defined type + Operations: procedure initialise(var S:stack); This procedure assigns an empty stack to S. procedure push(var S:stack;a:elemtype); 完整的 Stack S should not be full.This procedure adds the element a at the top of the stack. stack的 procedure pop(var S:stack); Stack S should not be empty.The top element of the stack is ADT removed. function top(S stack):elemtype; Stack S should be non-empty and this function returns the top element of the stack S.The stack S is left unchanged.(If elem- type is a structured type,this function should be rewritten as a procedure,see note 1 of section 3.1.) function empty(S:stack):boolean; This function returns true if S is empty and false otherwise. function full(S:stack):boolean; If S is full this function returns a true value. Otherwise it returns a false value
完整的 stack的 ADT
自然语言能够描述清楚ADT中各个成分吗？ Finally,since ADTs are mathematical objects,their meaning can be formally specified.Based on these specifications,it is then possible to verify that a given implementation of an ADT is correct and agrees with the specification. 狭义的程序设计中难得一见的科学内涵！
自然语言能够描述清楚ADT中各个成分吗？ 狭义的程序设计中难得一见的科学内涵！
Stack的数据部分的形式约束 stack::c integer (current time-point * max integer (maximum allowable size * 规约的数 据部分 elems pair-set (elems is a set of pairs * pair :object elemtype (object is of type elemtype * integer (t is a time-stamp * invariance 1:not [3a,b,t (a,t)eelems and (b,t)∈elems and 针对数据 的规约 a≠b] 生命周期 内保持 invariance 2:V(a,t)E elems c>t invariance 3:I elemsl max
Stack的数据部分的形式约束 针对数据 的规约 生命周期 内保持 规约的数 据部分