- more examples: BAG and INT
- equality of type instances
- consistency and completeness
- data type induction (example)
- what is an implementation?
- verifying an implementation
- example: algebra/implementation of STACK

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 :L07.n >Key=A END OF LECTURE L07 ?Again L07 ?Course