Report

Specification and Implementation of Abstract Data Types cs784(Prasad) 1 Spec v. Impl • (Functional) Specs should describe behavioral aspects only • Should ignore performance details • A “suitable implementation” requires client specific issues and trade-offs. • Even when you “can read” a suggested implementation from an Algebraic Spec, do not. • Distribution of work among the various operations is based on a chosen representation, which in turn is dictated by the pragmatics of an application. • In different implementations, some operations will be efficient while others won’t. 2 Data Abstraction • Clients – Need to know WHAT functions/services a module provides, – Not (should not be) HOW they are carried out. – So, ignore details irrelevant to the overall behavior, for clarity. • Implementors – May change the HOW (code), to improve performance, … – So, ensure that clients do not make unwarranted assumptions. cs784(Prasad) L34ADT 3 Specification of Data Types Type : Values + Operations Specify Syntax Semantics Signature of Ops Meaning of Ops Model-based Description in terms of standard “primitive” data types cs784(Prasad) Algebraic Axioms Give axioms defining the operations 4 Signatures of LISP S-expr Ops • • • • • • nil: S-expr cons: S-expr x S-expr S-expr car: S-expr S-expr cdr: S-expr S-expr null: S-expr boolean for every atom a: a : S-expr cs784(Prasad) 5 Signatures of LISP S-expr Ops • Signature tells us how to form complex terms from primitive operations. • Legal nil null(cons(nil,nil)) cons(car(nil),nil) • Illegal nil(cons) null(null) cons(nil) cs784(Prasad) L34ADT 6 Expectations of + : N x N N • A Few Examples • 1 + 2 = 3 • zero + succ(succ(zero)) = succ(succ(zero)) • x + 0 = x • Relating to Other Operators • 2 * (3 + 4) = 2 * 7 = 14 = 6 + 8 • x * ( y + z) = x * y + x * z cs784(Prasad) 7 What to expect of S-Expr ? • Examples • null(nil) = true • car(cons(nil,nil)) = nil • null(cdr(cons(nil,cons(nil,nil)))) = false • for all E,F in S-Expr • car(cons(E,F)) = E • null(cons(E,F)) = false cs784(Prasad) 8 Algebraic Specs of ADT • Operations on ADT – Constructors – Others • • • • Axioms: True statements about the ADT Algebraic Equational Axioms: LHS = RHS LHS: Application of Operations RHS: – similar to LHS, but – may also include if-expressions cs784(Prasad/pm) 9 Algebraic Specs of ADTs Characteristics of an “Adequate” Specification – Completeness (No “undefinedness”) – Consistency/Soundness (No conflicting definitions) GOAL: Learn to write sound and complete algebraic specifications of ADTs cs784(Prasad) L34ADT 10 Classification of Operations • Constructors – Generating values in the type • E.g., nil, cons, atoms a in ADT S-expr – Every value ought to be “constructible” • Non-constructors – E.g., car, cdr in ADT S-expr • Observers – Extract a value outside the type • E.g., null in ADT S-expr • Constructors: As few as possible cs784(Prasad) L34ADT 11 Stack ADT Operations • • • • • • createStack: → Stack push: Stack x element → Stack pop: Stack → Stack, element top: Stack → element isEmpty: Stack → boolean error an Element? cs784(pm) 12 Stack ADT Axioms 1. 2. 3. 4. 5. 6. isEmpty(createStack()) = true isEmpty(push(s, x)) = false top(createStack()) = error top(push(s, x)) = x pop(createStack()) = error pop(push(s, x)) = (s, x) cs784(pm) 13 S-Expr in LISP a : → S-Expr nil : → S-Expr cons : S-Expr x S-Expr → S-Expr car : S-Expr → S-Expr cdr : S-Expr → S-Expr null : S-Expr → boolean Observers : null Constructors : a, nil, cons Non-constructors : car, cdr cs784(Prasad) L34ADT 14 Algebraic Spec • Write equational axioms that characterize the meaning of all the operations. • Describe the meaning of the observers and the non-constructors on all possible constructor expressions. • Note the use of typed variables to abbreviate the definition. (“Finite Spec.”) cs784(Prasad) L34ADT 15 Algebraic Spec of S-expr • cdr(nil) = error • car(nil) = error • null(nil) = true cdr(a) = error car(a) = error null(a) = false • for all S, T in S-expr • null(cons(S,T)) = false • car(cons(S,T)) = S • cdr(cons(S,T)) = T • Omitting other equations for “nil” implies that implementations that differ only in the interpretation of “nil” are acceptable. Motivation for Minimal Constructors • If car and cdr are also regarded as constructors (as they generate values in the type), then the spec. must consider other cases to guarantee completeness (or provide sufficient justification for their omission). • for all S in S-expr: null(car(S)) = ... null(cdr(S)) = ... cs784(Prasad) L34ADT 17 ADT Table (aka symbol table/directory) • Signatures • empty: Table • update: Key × Info x Table Table • lookUp: Key × Table nfo • Equations • lookUp(K, empty) = error • lookUp(K, update(Ki, I, T)) = if K = Ki then I else lookUp(K,T) (“last update overrides the others”) • Note: Delete is missing. cs784(Prasad) 18 Table Examples • Constructions • empty • update(5, “abc”, empty) • update(10, “xyz”, update(5, “abc”, empty)) • update(5, “xyz”, update(5, “abc”, empty)) • Lookup Operations (Search ) • lookup (5, update(5, “xyz”, update(5, “abc”, empty)) ) • lookup (5, update(5, “xyz”, update(5, “xyz”, empty)) ) • lookup (5, update(5, “xyz”, empty) ) • Answer: “xyz” cs784(Prasad/pm) 19 Implementations of Table • “Different” implementations obeying the Algebraic Specs of Table. • Array-based • Linear List- based • Tree- based • Binary Search Trees, AVL Trees, B-Trees, etc. • Hash Table- based • Semantics of a client program is unchanged even when an implementation is replaced with another from the above. 20 Implementations of Table(cont’d) • Differ in performance aspects • search time • memory usage. • Other possible differences – Eliminating duplicates. – Retaining only the final binding. – Maintaining the records sorted on the key. – Maintaining the records sorted in terms of the frequency of use (a la caching). cs784(Prasad) L34ADT 21 A-list in LISP a : A nil : A-list cons : A x A-list A-list car : A-list A cdr : A-list A-list null : A-list boolean •Observers : •Constructors : •Non-constructors : cs784(Prasad) null, car nil, cons cdr 22 A-list in LISP • for all L in A-list – cdr(cons(a,L)) = L – car(cons(a,L)) = a – null(nil) = true – null(cons(a,L)) = false • Mostly silent about nil-list. cs784(Prasad) L34ADT 23 Natural Numbers zero : succ : add : x iszero : boolean observers : iszero constructors : zero, succ non-constructors : add Each number has a unique representation in terms of its constructors. cs784(Prasad) 24 Natural Numbers Axioms 1. 2. iszero(zero) = true iszero(succ(n)) = false 3. for all I,J in 4. add(zero, I) = I 5. add(succ(J), I) = succ(add(J,I)) cs784(Prasad) 25 Natural Numbers (cont’d) • add(succ(succ(zero)), succ(zero)) = succ(succ(succ(zero))) • The 4-th rule eliminates add from an expression, while the 5-th rule simplifies the first argument to add. • Associativity, commutativity, and identity properties of add can be deduced from this definition through deduction. cs784(Prasad/pm) 26 A-list Revisted a nil list append isnull :A : A-list : A A-list : A-list x A-list A-list : A-list boolean • Without cons/car/cdr • Example values – nil, list(a), append(nil, list(a)), ... cs784(Prasad) 27 Algebraic Spec of A-list • constructors – nil, list, append • observer isnull(nil) isnull(list(a)) = true = false isnull(append(L1, L2)) = isnull(L1) /\ isnull(L2) cs784(Prasad) L34ADT 28 A-list specification contd. • Problem : A value has multiple constructions. • Solution : Add axioms for constructors. – Identity Rule append(L, nil) = L append(nil, L) = L – Associativity Rule append(append(L1, L2), L3) = append(L1, append(L2, L3)) 29 Intuitive understanding of constructors • The constructor expressions correspond to distinct memory/data patterns required to store/represent values in the type. • The constructor axioms can be viewed operationally as rewrite rules to simplify constructor expressions. Specifically, constructor axioms correspond to computations necessary for equality checking and aid in defining a normal form. • Cf. cs784(Prasad) == vs equals in Java 30 General Strategy for ADT Specs • Constructors • Every value expected to be in the ADT must be constructible. • Non-constructors • Provide axioms to collapse a non-constructor term into a term involving only constructors. • Observers • Define the meaning of an observer on all constructor terms, checking for consistency. • Syntax • Specify signatures and classify operations. 31 Strategy for ADT Specs (contd) • Completeness • Define non-constructors and observers on all possible constructor patterns • Consistency • Check for conflicting reductions • Implementation of a type • An interpretation of the operations of the ADT that satisfies all the axioms. 32 Multiple Constructions for a Value • Write axioms to ensure that two constructor terms that represent the same value can be proven so. • E.g., identity, associativity, commutativity rules. 33 Declarative Specifications • Declare the desired item (using equations) by describing what properties it should have. • Did we define it “correctly”? • Can we determine what the defined item is? • A Famous Example • M(n) = if n > 100 then n – 10 else M(M(n+11)) fi 34 Decl Spec Examples • Let : N x N N denote an infix binary function • Equation: n n = n • Solution: n = 0 \/ n = 1. • = “multiplication” • Equation: n n = 0 • Solutions: n = 0 • = “multiplication”, • = “addition”, • = “subtraction”, … 35 delete: Set Set • for all n, m in N, s in Set • delete(n, empty) = empty • delete(n, insert(m, s)) = if (n = m) then delete(n, s) else insert(m, delete(n, s)) • Example: delete(5, insert(5, insert(5,empty)) ) = empty /= insert(5,empty) • Definitions along these lines for Tables capture “remove all occurrences” semantics. 36 delete: List List • “remove last occurrence” semantics • (For now imagine that “insert” is like prepend) • for all n, m in N, s in List • delete(n, empty) = empty • delete(n, insert(m, s)) = if (n = m) then s else insert(m, delete(n, s)) • Example: delete(5, insert(5,insert(5,empty)) ) = insert(5,empty) • “remove first/any/… occurrence” semantics is possible. • Questions: “first” and “last” based on what? Chronology? List representation? Is “insert” like prepend or append or something else? 37 size:List N v. size:Set N • size(insert(m, lst)) = 1 + size(lst) – E.g., size([2,2,2]) = 1 + size([2,2]) • size(insert(m, st)) = if (m in st) then size(st) else 1 + size(st) – E.g., size({2,2,2}) = size({2,2}) = size ({2}) = 1 38 OL: Ordered (N) Lists • Intuitively, • numbers in the list are ordered, and • no duplicates. • Constructors: • nil • ins : OL : N x OL OL • Non-constructors: • tl : OL OL • order : N_list OL • Observers: • null • hd : OL boolean : OL N 39 Expectations of OL • syntactically different, but semantically equivalent, constructor expressions • ins(2,ins(5,nil)) = ins(5,ins(2,nil)) • ins(2, ins(2, nil)) = ins(2, nil) • hd should return the smallest element. • May have no relation to the order of insertion. • Similarly for tl. cs784(Prasad/pm) 40 OL Axioms for Constructors • • • • • L is an ordered integer list; i, j in N null(nil) = true null(ins(I, L)) = false Idempotence: ins(i, ins(i,L)) = ins(i,L) Commutativity: ins(i, ins(j, L)) = ins(j, ins(j, L)) cs784(Prasad) 41 OL Axioms for Non-constructors • tl(nil) = error • tl(ins(I,L)) = 1. tl(ins(I, nil)) = nil 2. tl(ins(I, ins(J,L))) = a. I < J => ins(J, tl(ins(I,L)) ) b. I > J => ins(I, tl(ins(J,L)) ) c. I = J => tl( ins(I, L)) • (cf. constructor axioms for duplicate elimination) • order(nil) = nil • order(cons(I, L)) = ins(I, order(L)) cs784(Prasad) 42 OL Axioms for Observers • hd(nil) = error • hd(ins(I, nil)) = I • hd(ins(I,ins(J, L))) = • I < J => hd( ins(I, L) ) • I > J => hd( ins(J, L) ) • I = J => hd( ins(I, L) ) • null(nil) • null(ins(I, L)) cs784(Prasad) = = true false 43 Ordered List: Implementations • Representation Choice 1: – List of integers with duplicates • ins can be cons but then hd and tl require lineartime search • Representation Choice 2: – Sorted list of integers without duplicates • ins requires search but hd and tl can be made more efficient • Representation Choice 3: – Balanced-tree : Heap cs784(Prasad/pm) 44 Summary of ADT spec • Least common “denominator” of all possible implementations. • Focus on the essential behavior. • An implementation is a refinement of ADT spec. • IMPL = ADT + Representation “impurities” • To prove equivalence of two implementations, show that they satisfy the same ADT spec. • In the context of OOP, a class implements an ADT, and the spec. is a class invariant. 45 Advantages of ADT specs • Indirectly, ADT spec. gives us the ability to vary or substitute an implementation. – E.g., In the context of interpreter/compiler, a function definition and the corresponding calls (ADT FuncValues) together must achieve a fixed goal. However, there is freedom in the precise apportioning of workload between the two separate tasks: • How to implement/represent the function? • How to carry out the call? cs784(Prasad) L34ADT 46 Equality of Entities • Two viewpoints: v1 and v2 are equal, when • they can be proven to be equal • they cannot be proven that they are unequal • When a value can be multiply constructed, one of these constructions can be defined as a canonical form 47 Applications of ADT specs • ADT spec. are useful in automated formal reasoning about programs. • Provides a theory of equivalence of values that enables design of a suitable canonical form. • Identity • Associativity • Commutativity cs784(Prasad/pm) delete remove parenthesis sort 48