New version page

UF COP 5555 - Algebraic Spec

Upgrade to remove ads
Upgrade to remove ads
Unformatted text preview:

Algebraic Specification and Abstract Data TypesAlgebraic SpecificationAlgebraic Specification of the Data Type of Complex NumbersConsider the specification of a queue data typeFormal Mathematical Treatment of Abstract Data TypesQuotient AlgebraConsistency, Soundness, and CompletenessIntension, Extension, and Final AlgebrasAlgebraic 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)=xAlgebraic Specification of the Data Type of Complex Numberstype complex imports realoperations :+:complex Χ complex → complex-: complex Χ complex → complex*: complex Χ complex → complex/: complex Χ complex → complex-: complex → complexmakecomplex: real Χ real → complexrealpart: complex → realimaginarypart: complex → realvariables: x,y,z: complex; r,s: realaxioms:realpart(makecomplex(r,s)) = rimaginarypart(makecomplex(r,s)) = srealpart(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 typetype queue(element) imports booleanoperations:createq: queueenqueue: queue Χ element → queuedequeue: queue → queuefrontq: queue → elementemptyq: queue → booleanvariables: q: queue, x: elementaxioms:emptyq(createq) = trueemptyq(enqueue(q,x)) = falsefrontq(createq) = errorfrontq(enqueue(q,x)) = if emptyq(q) then x else frontq(q)dequeue(createq) = errordequeue(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:createqdequeue(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 relationis ≡, 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 ofempty(createq)=trueandempty(createq)=falsein 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 operations that can be applied to them.•Louden shows an array ADT example in which items that are intensionally different:insertIA(insertIA(createIA,1,1),2,2) -- AinsertIA(insertIA(createIA,2,2),1,1) -- Bare extensionally equivalentA = B iff for all i, extractIA(A,i) = extractIA(B,i)BAi

View Full Document
Download Algebraic Spec
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...

Join to view Algebraic Spec and access 3M+ class-specific study document.

We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Algebraic Spec 2 2 and access 3M+ class-specific study document.


By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?