Chapter 11

11.14
11.17
11.20
11.24

11.14 SymbolTable axioms
Write the axioms for an algebraic specification for an abstract data type SymbolTable with the following operations:

    create : SymbolTable
    enter : SymbolTable x name x value --> SymbolTable
    lookup : SymbolTable x name --> value
    isin : SymbolTable x name --> boolean


type SymbolTable(name, bindings) imports boolean

operations:


    create : SymbolTable
    enter : SymbolTable x name x value --> SymbolTable
    lookup : SymbolTable x name --> value
    isin : SymbolTable x name --> boolean

variables: s: SymbolTable, n: name, b: bindings

axioms:
     enter(s, n, b) = s
     lookup(s, n) = b
     lookup(create, n) = false
     isin(create, n) = false
     isin(s, n) = if lookup(s,n) then true else false

11.17 bstree axioms
Write an algebraic specification for an abstract data type bstree (binary search tree) with the following operations:

     create: bstree
     make: bstree x element 3 bstree --> bstree
     empty: bstree --> boolean
     left: bstree --> bstree
     right: bstree -->bstree
     data: bstree --> element
     isin: bstree x element --> boolean
     insert: bstree x element --> bstree

variables: b: bstree, e: element

axioms:

     make(create, (left(data(bstree)), right(data(bstree)), data(bstree)) = b
     empty(create) = true
     empty(insert(b, e) = false
     left(s) = s
     right(s) = s
     data(s) = e
     isin(s, e) = if data(s) then true else false
     isin(create, e) = false
     insert(s, e) = s

For this to be possible, we need to know about the bstree's element data type. how can we traverse it. Is it doubly-linked, singly-linked or is it an array? Once we know that information we can create valid functions.

11.20 Queue axioms

a) frontq(enqueue(enqueue(createq,x),y) = x is true because of the following axioms and operations
     frontq(enqueue(q,x) = if emptyq(q) then x else frontq(q)
     enqueue: queue x element --> queue
    
since enqueue takes a queue and an element, the inner parameters of frontq are nested and valid, then we have an element.

b) Since the dequeue takes a queue and the enqueue returns a queue, this call is valid.
c) frontq takes a queue which dequeue satisfies.

11.24 Stack axioms

operations:
     full: stack --> boolean
     size: stack --> integer
     maxsize: integer

axioms:
     full(s) = if size(s) >= maxsize true else false
     plus the rest of the axioms