Algebraic Specifications and Abstract Data Types OVERVIEW Algebraic Specs and Axiomatic Proofs Many-Sorted Algebras Syntax and Semantics of Specification Example: STACK type Example: SET type ASSIGNMENT: A6* ?Course ?Lecture L06.1 ?"Next Lecture" L07 :L06.1 WHAT ARE ALGEBRAIC SPECS? Up to now have seen axiomatic proof of programs with very simple data (integers) Exception: arrays... structured data The behavior of an array is unambiguously defined by the designer of a programming language. Inference rules and axioms for arrays (and for records and other built-in structured types) can be designed from the language definition. So we can do axiomatic proofs with arrays, records, etc. :L06.1.1 USER-DEFINED TYPES What about types that are user-defined, that are not built-in to a programming language? Where is the definition of their behavior so we can get axioms and inference rules for them? We need a way of specifying the behavior of user-defined types so that their properties can be used during verification of programs that use those types. :L06.1.2 USER-DEFINED TYPES Specs of user-defined data types must be abstract, that is, they must state behavior and logical properties without bias towards low-level details: Example: Suppose we need to specify the behavior of a data type STACK, with ops push, pop, etc... If we specify something like push(S,e) is S[(top+=1)] := e pop(S) is top -= 1 we imply in the specs that a STACK is an array at the low implementation level... What if we wanted to build STACK as a linked list? Specs should not prefer or exclude any reasonable implementation method... L06.2 ALGEBRAIC SPECS and AXIOMATIC VERIFICATION We will specify the behavior of a user-defined type as a many-sorted algebra Many-sorted algebra is -- collection of elements of various types (types are called "sorts") -- operations that manipulate these elements :L06.2.1 ALGEBRAIC SPECS and AXIOMATIC VERIFICATION Specification has three main parts: -- syntax (what are the sorts, ops, arguments) -- semantics (what do the ops do?) -- restrictions (are there exceptions or limits?) Semantics component provide axioms that can be used in axiomatic proofs of programs that use the specified type :L06.3 EXAMPLE: ALGEBRAIC SPECIFICATION of QUEUE (Syntax) sorts: QUEUE, INT, BOOLEAN operations: new: --> QUEUE add: QUEUE x INT --> QUEUE del: QUEUE --> QUEUE head: QUEUE --> INT U { error } empty: QUEUE --> BOOLEAN :L06.3.1 EXAMPLE: ALGEBRAIC SPECIFICATION of QUEUE (Syntax) sorts: QUEUE, INT, BOOLEAN operations: new: --> QUEUE add: QUEUE x INT --> QUEUE del: QUEUE --> QUEUE head: QUEUE --> INT U { error } empty: QUEUE --> BOOLEAN EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Syntax) sorts: STACK, INT, BOOLEAN operations: new: --> STACK push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.3.2 >.window[text 5 6 8 50] >.titles[off] Note that these two syntax specfications have essentially the same form... they differ in the name QUEUE becoming STACK, and the names of the operations being a bit different... But, clearly, STACK and QUEUE are two very different data types... STACK is LIFO, and QUEUE is FIFO, for example This behavioral difference is captured not in the syntax, but in the semantic component of an algebraic specification. ?Back .window[text] L06.4 :L06.4 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) :L06.5 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.6 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.7 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S top(new()) = error top(push(S,i)) = i new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.8 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S top(new()) = error top(push(S,i)) = i empty(new()) = true empty(push(S,i)) = false new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.8.0 >.window[text 5 5 9 52] >.title[top left COMMENTS ON AXIOMS] no implementation implied here cannot get a feel for, say, how "push" affects a stack by examining one, or a few, axioms. In operational specs, you can. ?More .window[text] L06.8.0.1 :L06.8.0.1 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S top(new()) = error top(push(S,i)) = i empty(new()) = true empty(push(S,i)) = false new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK top: STACK --> INT U { error } empty: STACK --> BOOLEAN :L06.8.1 >.window[text 5 5 9 52] >.title[top left HOW DOES ONE KNOW WHEN TO STOP?] generator an operation of the specified type that is necessary to construct any specific instance of the type obviously, an operation that produces an element of a sort other than the specified type cannot be a generator ?More .window[text] L06.9 :L06.9 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S top(new()) = error top(push(S,i)) = i empty(new()) = true empty(push(S,i)) = false new: --> STACK (operations) push: STACK x INT --> STACK pop: STACK --> STACK x top: STACK --> INT U { error } x empty: STACK --> BOOLEAN :L06.10.1 >.window[text 5 5 10 51] >.title[top left new / push / pop ?] "new" is obviously a generator, since it is the only operation that creates an original STACK (push(pop(push(push(new(),4),7)),3) produces the same stack instance as (push(push(new(),4),3) Any stack that can be built using "pop" can also be built another way without "pop". Concept: "canonical representation" Consider the stack "3 4 (bottom)", that is, with two elements, 3 on top and 4 on bottom... (push(push(new(),4),3) in canonical form (push(pop(push(push(new(),4),7)),3) not ?More .window[text] L06.11 :L06.11 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() pop(push(S,i)) = S top(new()) = error top(push(S,i)) = i empty(new()) = true empty(push(S,i)) = false new: --> STACK (operations) push: STACK x INT --> STACK x pop: STACK --> STACK x top: STACK --> INT U { error } x empty: STACK --> BOOLEAN :L06.12 >.window[text 5 5 6 51] >.title[top left AXIOM CONSTRUCTION HUERISTIC] Once generators have been identified, enumerate left-hand-sides for axioms by all combinations of a non-generator applied to the result of a generator examine each left-hand-side so produced and construct a right-hand-side that describes an equivalent, but differently stated, structure. each axiom is an equation... LHS = RHS thus axioms are rewrite rules... tell how to take a sequence of operations from the algebra and transform to new (shorter, simpler) sequence. ?More .window[text] L06.13 :L06.13 EXAMPLE: ALGEBRAIC SPECIFICATION of STACK (Semantics) pop(new()) = new() | pop(push(S,i)) = S | see how these | axioms were generated top(new()) = error | by the hueristic top(push(S,i)) = i | | empty(new()) = true | empty(push(S,i)) = false | new: --> STACK (operations) push: STACK x INT --> STACK x pop: STACK --> STACK x top: STACK --> INT U { error } x empty: STACK --> BOOLEAN :L06.14 ANOTHER EXAMPLE: SET of INT :L06.15 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN :L06.16 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET delete: SET x INT --> SET member: SET x INT --> BOOLEAN :L06.17 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN :L06.18 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) member(insert(S,j),k) :L06.19 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) member(insert(S,j),k) delete(empty(),j) delete(insert(S,j),k) :L06.20 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) = false member(insert(S,j),k) delete(empty(),j) delete(insert(S,j),k) :L06.21 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) = false member(insert(S,j),k) = if (j=k) then true else member(S,k) delete(empty(),j) delete(insert(S,j),k) :L06.22 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) = false member(insert(S,j),k) = if (j=k) then true else member(S,k) delete(empty(),j) = empty() delete(insert(S,j),k) :L06.23 ANOTHER EXAMPLE: SET of INT sorts: SET, INT, BOOLEAN operations: empty: --> SET insert: SET x INT --> SET x delete: SET x INT --> SET x member: SET x INT --> BOOLEAN axioms member(empty(),j) = false member(insert(S,j),k) = if (j=k) then true else member(S,k) delete(empty(),j) = empty() delete(insert(S,j),k) = if (j=k) then delete(S,j) else insert(delete(S,k),j) :L06.n >Key=A END OF LECTURE L06 ?Again L06 ?Course ?"Next Lecture" L07 :L07 >Key=L L07: Verification of Abstract Data Types OVERVIEW more examples: BAG and INT equality of type instances consistency and completeness data type induction what is an implementation? verifying an implementation example: algebra/implementation of STACK ASSIGNMENT: A7* ?Course ?Lecture L07.1 ?"Next Lecture" L08 :L07.1 ANOTHER ALGEBRA: type BAG (multiset) sorts: BAG, INT, BOOLEAN operations: empty: --> BAG insert: BAG x INT --> BAG delete: BAG x INT --> BAG member: BAG x INT --> BOOLEAN :L07.1.1 ANOTHER ALGEBRA: type BAG (multiset) sorts: BAG, INT, BOOLEAN operations: empty: --> BAG insert: BAG x INT --> BAG x delete: BAG x INT --> BAG x member: BAG x INT --> BOOLEAN :L07.2 ANOTHER ALGEBRA: type BAG (multiset) sorts: BAG, INT, BOOLEAN operations: empty: --> BAG insert: BAG x INT --> BAG x delete: BAG x INT --> BAG x member: BAG x INT --> BOOLEAN axioms member(empty(),i) member(insert(B,i),j) delete(empty(),i) delete(insert(B,i),j) :L07.3 ANOTHER ALGEBRA: type BAG (multiset) sorts: BAG, INT, BOOLEAN operations: empty: --> BAG insert: BAG x INT --> BAG x delete: BAG x INT --> BAG x member: BAG x INT --> BOOLEAN axioms member(empty(),i) = false member(insert(B,i),j) = if (i=j) then true else member(B,j) delete(empty(),i) = empty() delete(insert(B,i),j) = if (i=j) then B else insert(delete(B,j),i) :L07.4 >.window[text 4 6 10 48] >.titles[off] The essential difference between SET and BAG is captured in the "delete(insert ... )" axiom. delete an item after inserting that item always returns the original BAG... not necessarily so for SET. ?Continue .window[text] L07.5 :L07.5 ANOTHER EXAMPLE: type INT sorts: INT, BOOLEAN operations: zero: --> INT succ: INT --> INT add: INT x INT --> INT equal: INT x INT --> BOOLEAN :L07.5.0 >.window[text 7 6 10 50] >.title[top left CANONICAL FORM] We will use Church's representation for integers, that is, every integer K is obtained by taking the Kth successor of the zero element. Our operation "zero()" creates the zero element for our algebra: 0 = zero(). example: the integer 4 is represented as 3 = succ( succ( succ( zero() ) ) ) ?More .window[text] L07.5.0.1 :L07.5.0.1 ANOTHER EXAMPLE: type INT sorts: INT, BOOLEAN operations: zero: --> INT succ: INT --> INT x add: INT x INT --> INT x equal: INT x INT --> BOOLEAN :L07.5.1 >.window[text 12 6 5 50] >.title[top left MORE ON THE AXIOM HUERISTIC] In earlier examples we created one axiom for every combination of a non-generator applied to a generator. Now we see that sometimes each combination may create several axioms... it depends on how many arguments of the same type occurr in the operations... ?Continue .window[text] L07.6 :L07.6 ANOTHER EXAMPLE: type INT sorts: INT, BOOLEAN operations: zero: --> INT succ: INT --> INT x add: INT x INT --> INT x equal: INT x INT --> BOOLEAN :L07.7 ANOTHER EXAMPLE: type INT sorts: INT, BOOLEAN operations: zero: --> INT succ: INT --> INT x add: INT x INT --> INT x equal: INT x INT --> BOOLEAN axioms add(zero(),zero()) add(succ(n),zero()) add(zero(),succ(n)) add(succ(n),succ(m)) equal(zero(),zero()) equal(succ(n),zero()) equal(zero(),succ(n)) equal(succ(n),succ(m)) :L07.8 ANOTHER EXAMPLE: type INT sorts: INT, BOOLEAN operations: zero: --> INT succ: INT --> INT x add: INT x INT --> INT x equal: INT x INT --> BOOLEAN axioms add(zero(),zero()) = zero() add(succ(n),zero()) = succ(n) add(zero(),succ(n)) = succ(n) add(succ(n),succ(m)) = succ(succ(add(n,m)) equal(zero(),zero()) = true equal(succ(n),zero()) = false equal(zero(),succ(n)) = false equal(succ(n),succ(m)) = equal(n,m) :L07.9 DATA TYPE INDUCTION use to prove that some property P holds for every element of some type T. similar technique to mathematical induction take operations that map to the type, and separate them into a) those that have no arguments of type T b) those that do have arguments of type T will show our goal by showing that every element of T has property P when it is first created (point (a) above) and that every time it is transformed (point (b) above) it retains the property P... :L07.10 DATA TYPE INDUCTION (continued) basis: show P holds for the result of each operation that maps to type T but needs no args of type T induction: show for each other operation mapping to type T that if P holds for the args of type T, then it also holds for the result. Example: STACK basis: show P(new()) induction: show P(S) ==> P(push(S,i)) for arbitrary i show P(S) ==> P(pop(S)) :L07.11 >.window[text 3 5 8 51] >.title[top left NORMAL FORM LEMMA] can use our canonical (normal) form to ease these proofs.. If we have proven a normal form lemma (used informally up to now) we can do the DT Induction for generators only, instead of for all operations mapping to the type. STACK: normal form lemma is forall S in STACK, either S = new() or S = push(...(push(new(),e1)...),en) ?More .window[text] L07.12 :L07.12 DATA TYPE INDUCTION (continued) basis: show P holds for the result of each operation that maps to type T but needs no args of type T induction: show for each other operation mapping to type T that if P holds for the args of type T, then it also holds for the result. Example: STACK basis: show P(new()) induction: show P(S) ==> P(push(S,i)) for arbitrary i show P(S) ==> P(pop(S)) :L07.13 DATA TYPE INDUCTION (continued) basis: show P holds for the result of each operation that maps to type T but needs no args of type T induction: show for each other operation mapping to type T that if P holds for the args of type T, then it also holds for the result. Example: STACK (normal form) basis: show P(new()) induction: show P(S) ==> P(push(S,i)) for arbitrary i :L07.14 EXAMPLE DATA TYPE INDUCTION UDIR: UNIX Directory sorts: UDIR, INT, ID, BOOLEAN operations: /: --> UDIR mkdir: UDIR x ID --> UDIR cd: UDIR x ID --> UDIR pwd: UDIR --> ID up: UDIR x INT --> ID isName: ID --> BOOLEAN :L07.15 >.window[text 11 5 7 51] >.title[top left CANONICAL FORM] For UDIR, the generators are /, mkdir, cd. / makes the root of a directory tree. mkdir hangs subtrees off a directory. cd changes the current location. The operation "isName" is auxiliary, that is, it will be used in the axioms, but is not a visible operation of the type. operation: isName("..") = false, otherwise true this allows ".." to be a special ID we will use ".." to mean "parent" ?More .window[text] L07.16 :L07.16 UDIR: UNIX Directory sorts: UDIR, INT, ID, BOOLEAN operations: /: --> UDIR mkdir: UDIR x ID --> UDIR cd: UDIR x ID --> UDIR x pwd: UDIR --> ID x up: UDIR x INT --> ID * isName: ID --> BOOLEAN ================================================================= Verifying implementations of Algebraic Specs OVERVIEW Example: Unix DIrectory UDIR Data type induction verifying an implementation ASSIGNMENT: A8* ?Course ?Lecture L08.1 ?"Next Lecture" L09 :L08.1 UDIR: UNIX Directory sorts: UDIR, INT, ID, BOOLEAN operations: /: --> UDIR mkdir: UDIR x ID --> UDIR cd: UDIR x ID --> UDIR x pwd: UDIR --> ID x up: UDIR x INT --> ID * isName: ID --> BOOLEAN :L08.2 UDIR: UNIX Directory sorts: UDIR, INT, ID, BOOLEAN operations: /: --> UDIR mkdir: UDIR x ID --> UDIR cd: UDIR x ID --> UDIR x pwd: UDIR --> ID x up: UDIR x INT --> ID * isName: ID --> BOOLEAN axioms pwd(/) = pwd(mkdir(D,i) = pwd(cd(D,i)) = up(/,n) = up(mkdir(D,i),n) = up(cd(D,i),n) = :L08.3 UDIR: UNIX Directory sorts: UDIR, INT, ID, BOOLEAN operations: /: --> UDIR mkdir: UDIR x ID --> UDIR cd: UDIR x ID --> UDIR x pwd: UDIR --> ID x up: UDIR x INT --> ID * isName: ID --> BOOLEAN axioms pwd(/) = "/" pwd(mkdir(D,i) = pwd(D) pwd(cd(D,i)) = if isName(i) then up(D,1) else i up(/,n) = "/" up(mkdir(D,i),n) = up(D,n) up(cd(D,i),n) = if isName(i) then up(D,n-1) else up(D,n+1)