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.
Where is the definition of their behavior so we can get axioms and inference rules for them?
If we specify something like
push(S,e) is S[(top+=1)] := e pop(S) is top -= 1we imply in the specs that a STACK is an array at the low implementation level...
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
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 (axioms) of an algebraic specification.
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)