Algebraic Specifications for STACK
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
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)