2008-2-181CSE 3302 Programming LanguagesAbstract Data Types Chengkai Li, Weimin HeSpring 2008and ModulesLecture 11 – ADT and Modules, Spring 20081CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 2008Data Types• Predefined• Type constructors: build new data types• How to provide “queue”?– What should be the data values?– What should be the operations?– How to implement (data representation, operations)?Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20082What are inadequate here?• The operations are not associated with the data type– You can use the operation on an invalid value.• Users see all the details:direct access to date elements, implementations– Implementation dependent– Users can even mess up with thingsLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20083What do we want?• For basic types:– 4 bytes or 2 bytes, users don’t need to know.– Can only use predefined operations.• Similarly, for the “Queue” data type:?Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20084Abstract Data Type• Encapsulation:all definitions of allowed operations for a data type in one place.• Information Hiding:separation of implementation details from definitions. Hide the details .Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20085Algebraic Specification of ADT• Syntactic specification (signature, interface):the name of the type, the prototype of the operations• Semantic specification (axioms, implementation):guide for required properties in implementationmathematical properties of the operationsThey don’t specify:– data representation– implementation detailsLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200862008-2-182Syntactic Specificationtype queue(element) imports booleanoperations:createq: queueenqueue: queue × element → queuedequeue: queue → queuefrontq: queue → elementemptyq: queue → boolean• imports: the definition queue needs boolean• Parameterized data type (element)• createq: not a function, or viewed as a function with no parameterLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20087Algebraic Specificationvariables: q: queue; x: elementaxioms:emptyq(createq) = trueemptyq(enqueue(q,x)) = falsefrontq(createq) = errorfrontq(enqueue(q,x)) = if emptyq(q) then xelse frontq(q)dequeue(createq) = errordequeue(enqueue(q,x)) = if emptyq(q) then qelse enqueue(dequeue(q),x)• error axiom (exceptions)Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20088Stacktype stack(element) imports booleanoperations:createstk : stackpush : stack × element → stackpop : stack → stacktop : stack → elementemptystk: stack→booleanLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 20089emptystk: stack →booleanvariables: s: stack; x: elementaxioms:emptystk(createstk) = trueemptystk(push(s,x)) = falsetop(createstk) = errortop(push(s,x)) = xpop(createstk) = errorpop(push(s,x)) = sAxioms• How many axioms are sufficient for proving all necessary properties?Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200810Some Heuristicstype stack(element) imports booleanoperations:createstk : stackpush : stack × element → stackpop : stack → stacktop : stack → elementemptystk: stack→booleanConstructor:createstkpushLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200811emptystk: stack →booleanvariables: s: stack; x: elementaxioms:emptystk(createstk) = trueemptystk(push(s,x)) = falsetop(createstk) = errortop(push(s,x)) = xpop(createstk) = errorpop(push(s,x)) = sInspector:poptopemptystk2 * 3 = 6 rulesBinary Search Treetype BST(element) imports boolean, intoperations:createbst : BSTemptybst : BST → booleaninsert : BST × element → BSTdelete : BST × element → BSTgetRoot: BST→elementgetRoot: BST→elementgetHeight : BST → intmax : BST → elementsearch : BST × element → booleanvariables: t: bst; x: elementaxioms:emptystk(createbst) = true…Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 2008122008-2-183Other Examples of ADT• Stack• Queue• Tree• SetLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200813• Map• Vector• List• Priority Queue• Graph• …ADT Mechanisms• Specific ADT mechanisms– ML abstype• General module mechanism : not just about a single data type and its operationssingle data type and its operations– Separate compilation and name control:C, C++, Java– Ada, ML• Class in OO languagesLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200814ML Abstypeabstype 'element Queue = Q of 'element listwithval createq = Q [];fun enqueue(Q lis, elem) = Q(lis @ [elem]);fun dequeue(Q lis) = Q(tl lis);fun frontq(Q lis) = hd lis;fun emptyq(Q []) = true |emptyq(Q(h::t)) = false;end;Lecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200815end;type 'a Queueval createq = - : 'a Queueval enqueue = fn : 'a Queue * 'a -> 'a Queueval dequeue = fn : 'a Queue -> 'a Queueval frontq = fn : 'a Queue -> 'aval emptyq = fn : 'a Queue -> bool- val q = enqueue(createq,3);Val q = - : int QueueModules• Module: A program unit with a public interface and a private implementation; all services that are available from a module are described in its public interface and are exported to other modules, and all services that are needed by a module must be imported from other modules.• In addition to ADT, module supports structuring of large programs: Separate compilation and name controlLecture 11 – ADT and Modules, Spring 2008CSE3302 Programming Languages, UT-Arlington ©Chengkai Li, Weimin He, 200816C: Separate Compilation• queue.h : header file#ifdef QUEUE_H#define QUEUE_Hstruct
View Full Document
Unlocking...