Transcript Algebraic Specification and Abstract Data Types

Algebraic Specification and
Abstract Data Types
• An abstract data type is typically characterized
by a set of operations that
–
–
–
–
construct structured data from primitive data
extract primitive data from a data structure
modify the contents of a data structure
test properties of the data structure
• Programming languages providing abstract data
types provide constructs to
– represent the specification of the data type and its
operations
– implement the representation of the data type and
operations upon it.
Algebraic Specification
• An algebra is specified by giving a sort (this is the name
of a set), and a set of signatures (this is a set of function
specifications).
• For example, think of a simple algebra for arithmetic with
addition and subtraction:
<S,{+:S Χ S → S, -:S Χ S → S}>
• The specification of an algebra is an abstract entity. We
can create a associate a particular algebra with the
specification by associating a set (called the carrier set)
with the sort and a specific function with each operator
symbols in the signatures.
• Properties of any particular algebra (or model of an
algebra) are specified by giving axioms such as
-(+(x,y),y)=x
Algebraic Specification of the Data
Type of Complex Numbers
type complex imports real
operations:
+:complex Χ complex → complex
-: complex Χ complex → complex
*: complex Χ complex → complex
/: complex Χ complex → complex
-: complex → complex
makecomplex: real Χ real → complex
realpart: complex → real
imaginarypart: complex → real
variables: x,y,z: complex; r,s: real
axioms:
realpart(makecomplex(r,s)) = r
imaginarypart(makecomplex(r,s)) = s
realpart(x+y) = realpart(x) + realpart(y)
...
• There are actually some problems with this specification. For
example, how can it handle division by 0 (which yields an error)?
Consider the specification of a
queue data type
•
•
•
•
•
type queue(element) imports boolean
operations:
createq: queue
enqueue: queue Χ element → queue
dequeue: queue → queue
frontq: queue → element
emptyq: queue → boolean
variables: q: queue, x: element
axioms:
emptyq(createq) = true
emptyq(enqueue(q,x)) = false
frontq(createq) = error
frontq(enqueue(q,x)) = if emptyq(q) then x else frontq(q)
dequeue(createq) = error
dequeue(enqueue(q,x)) = if emptyq(q) then q else
enqueue(dequeue(q),x)
Note the use of a data type parameter, element
If you look at the signature of frontq, you see that it’s supposed to return a boolen, but axiom 3
requires that it be able to return something called error. This axiom does not follow the rules.
Note a similar problem for dequeue. Louden introduces the idea of a constructor (that creates a
new object of the data type being defined) and an inspector (that retrieves previously constructed
values).
But note that dequeue is defined constructively, in terms of the queue value that it returns which is
created by calling enqueue. Evaluate dequeue(enqueue(enqueue(enqueue(createq,1),2),3),4) to
see why I consider dequeue to be a constructor!
In Louden’s nomenclature, frontq is a selector, and emptyq is a predicate.
Formal Mathematical Treatment of
Abstract Data Types
• The nomenclature used in formal discussions of ADTs is borrowed
from Algebra and Logic.
• An ADT specification describes an existential (or potential) type
because it asserts the existence of an actual type without really
demonstrating that such an actual type really exists.
• Any actual type that satisfies the axioms of an ADT is said to be a
model of the ADT.
• Given a carrier set, we can construct the free algebra of terms for
the algebra. This is the set of all valid combinations of the
operations:
createq
dequeue(createq)
enqueue(createq,1)
dequeue(enqueue(createq,1))
enqueue(enqueue(createq, 1),2)
...
Quotient Algebra
• We can furthermore construct the quotient algebra of the
equivalence relation generated by the equational axioms
by
– identifying a normal order for the terms in the free algebra
– removing any term tn that is equivalent (under the axioms) to a
lower order term tm.
If our algebra is F and our equivalence relation
is ≡, the quotient algebra is denoted F/≡.
• The quotient algebra of a specification is known as its
initial algebra.
• Elements in the initial algebra are assumed to be unique
unless it can somehow be proven that they are
equivalent.
Consistency, Soundness, and
Completeness
• A theory or proof system is said to be consistent if it does not
contain both the terms A and ~A. Given our queue specification, we
can’t, for example, have both of
empty(createq)=true
and
empty(createq)=false
in the initial algebra.
• A theory is said to be sound if any statement that can be proven is
true (that is, if any outcome of application of the axioms is in the
model). Because of the way we construct an initial algebra from the
carrier set and the signatures, it will necessarily be sound.
• A theory is said to be complete if any true statement can be proven
from the axioms. When Louden says this means the initial algebra
is not too small, he’s saying that the initial algebra hasn’t left out any
true statements. Any model of the algebra will be an actual data
type. If something is true of every model of the algebra, yet, it
cannot be proven from the axioms, then the set of axioms is
incomplete.
Intension, Extension, and Final
Algebras
• Two objects are said to be equivalent in
intension if their representation is the same.
• Two objects are said to be equivalent in
extension if they cannot be distinguished by any
A, B
operations that can bei,applied
to them.
• Louden shows an array ADT example in which
items that are intensionally different:
insertIA(insertIA(createIA,1,1),2,2) -- A
insertIA(insertIA(createIA,2,2),1,1) -- B
are extensionally equivalent
A = B iff for all i, extractIA(A,i) = extractIA(B,i)