Specification and Implementation of Abstract Data TypesData AbstractionAbstraction : Equivalence RelationsSpecification of Data TypesSyntax of LISP S-exprSlide 6Formal Spec. of ADTsClassification of OperationsADT Table (symbol table/directory)ImplementationsA-list in LISPAlgebraic SpecSlide 13Natural NumbersSlide 15A-list RevistedSlide 17Slide 18Writing ADT SpecsGeneral Strategy for ADT SpecsSlide 21Model-based vs AlgebraicExampleCanonical Form for Equality TestingOrdered Integer ListsSlide 26Axioms for ConstructorsAxioms for Non-constructorsAxioms for ObserversObject-Oriented Software Constructionceg860 (Prasad) LADT 1Specification and Implementation of Abstract Data TypesAlgebraic Techniquesceg860 (Prasad) LADT 2Data Abstraction•Clients –Interested in WHAT services a module provides, not HOW they are carried out. So, ignore details irrelevant to the overall behavior, for clarity.•Implementors–Reserve the right to change the code, to improve performance. So, ensure that clients do not make unwarranted assumptions.ceg860 (Prasad) LADT 3Abstraction : Equivalence Relations–Computability•Recursive vs Non-recursive–Semantics•Behavioral Equivalence–Resource-independent interchangeability•Performance aspect irrelevant for “correctness”–E.g., Groups, Fields, Sorting, UNIX, etc–Algorithms•Time and Space requirements–Big-Oh (Worst-case Analysis)–NP-hard vs Polynomial-timeceg860 (Prasad) LADT 4Specification of Data Types Type : Values + Operations Specify Syntax Semantics Signature of Ops Meaning of Ops Model-based Axiomatic(Algebraic) Description in terms of Give axioms satisfied standard “primitive” data types by the operationsceg860 (Prasad) LADT 5Syntax of LISP S-expr•operations: nil, cons, car, cdr, null•signatures: nil: S-exprcons: S-expr  S-expr  S-expr car: S-expr  S-exprcdr: S-expr  S-exprnull: S-expr booleanfor every atom a: a : S-exprceg860 (Prasad) LADT 6•Signature tells us how to form complex terms from primitive operations.•Legalnilnull(cons(nil,nil))cons(car(nil),nil)•Illegalnil(cons)null(null)cons(nil)ceg860 (Prasad) LADT 7 Formal Spec. of ADTsCharacteristics of an “Adequate” Specification–Completeness (No undefinedness)–Consistency/Soundness (No conflicting definitions)GOAL: Learn to write sound and complete algebraic(axiomatic) specifications of ADTsceg860 (Prasad) LADT 8Classification of Operations•Observers (“Queries”)–generate a value outside the type•E.g., null in ADT S-expr•Constructors (“Creators and Commands”)–required for representing values in the type•E.g., nil, cons, atoms a in ADT S-expr•Non-constructors (“Creators and Commands”)–remaining operations•E.g., car, cdr in ADT S-exprceg860 (Prasad) LADT 9ADT Table (symbol table/directory)empty : Tableupdate : Key x Info x Table TablelookUp: Key x Table nfolookUp(K,empty) = error(Use of variable)(Alternative : Use of Preconditions)lookUp(K,update(Ki, I, T)) = if K = Ki then I else lookUp(K,T)(“last update overrides the others”)ceg860 (Prasad) LADT 10Implementations–Array-based–LinearList-based–Tree-based•Binary Search Trees, AVL Trees, B-Trees etc–HashTable-based•These exhibit a common Table behavior, but differ in performance aspects.•Correctness of a client program is assured even when the implementation is changed.ceg860 (Prasad) LADT 11A-list in LISP a : Anil : A-listcons : A x A-list A-listcar : A-list A cdr : A-list A-listnull : A-list boolean•Observers : null, car•Constructors : nil, cons•Non-constructors : cdrceg860 (Prasad) LADT 12Algebraic Spec•Write axioms (equations) that characterize the meaning of all the operations. •Describe the meaning of the observers and the non-constructors on all possible constructor patterns.•Note the use of typed variables to abbreviate the definition. (“Finite Spec.”)ceg860 (Prasad) LADT 13• for all S, T in S-expr cdr(nil) = error cdr(cons(S,T)) = T car(nil) = error car(cons(S,T)) = S null(nil) = true null(cons(S,T)) = false(To avoid “error”, use preco nditions instead.)•Other atoms “a” are handled in the same way as “nil”.ceg860 (Prasad) LADT 14Natural Numberszero : succ :  add :  x  iszero :  booleanobservers : iszeroconstructors : zero, succnon-constructors : addEach numbers has a unique representation in terms of its constructors.ceg860 (Prasad) LADT 15for all I,J in add(zero,I) = Iadd(succ(J), I) = succ(add(J,I))iszero(zero) = trueiszero(succ(n)) = falseceg860 (Prasad) LADT 16A-list Revisted a : Anil : A-listlist : A A-listappend : A-list x A-list A-listnull : A-list boolean• values – nil, list(a), append(nil, list(a)), ...ceg860 (Prasad) LADT 17Algebraic Spec•constructors–nil, list, append•observerisnull(nil) = trueisnull(list(a)) = falseisnull(append(L1,L2)) = isnull(L1) /\ isnull(L2)ceg860 (Prasad) LADT 18•Problem : Same value has multiple representation in terms of constructors.•Solution : Add axioms for constructors.–Identity Ruleappend(L,nil) = Lappend(nil,L) = L–Associativity Rule append(append(L1,L2),L3) = append(L1, append(L2,L3))ceg860 (Prasad) LADT 19Writing ADT Specs•Idea: Specify “sufficient” axioms such that syntactically distinct patterns that denote the same value can be proven so.–Completeness•Define non-constructors and observers on all possible constructor patterns–Consistency•Check for conflicting reductions•Note: A term essentially records the detailed history of construction of the value.ceg860 (Prasad) LADT 20General Strategy for ADT Specs•Syntax–Specify signatures and classify operations.•Constructors–Write axioms to ensure that two constructor terms that represent the same value can be proven so.•E.g., identity, associativity, commutativity rules.ceg860 (Prasad) LADT 21•Non-constructors–Provide axioms to collapse a non-constructor term into a term involving only constructors.•Observers–Define the meaning of an