home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #1 / NN_1993_1.iso / spool / comp / specific / 603 < prev    next >
Encoding:
Internet Message Format  |  1993-01-06  |  3.4 KB
  1. Path: sparky!uunet!pipex!bnr.co.uk!uknet!edcastle!dcs.ed.ac.uk!dts
  2. From: dts@dcs.ed.ac.uk (Don Sannella)
  3. Newsgroups: comp.specification
  4. Subject: Re: Theoretical limitations of algebraic specifications?
  5. Keywords: Specification,Algebraic
  6. Message-ID: <C0FsG5.5L3@dcs.ed.ac.uk>
  7. Date: 6 Jan 93 14:33:40 GMT
  8. References: <1992Dec31.000439.8884@gmuvax2.gmu.edu>
  9. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  10. Organization: Department of Computer Science, University of Edinburgh
  11. Lines: 58
  12.  
  13. In article <1992Dec31.000439.8884@gmuvax2.gmu.edu>, ofut@gmuvax2.gmu.edu (A. Jeff Offutt) writes:
  14. > Generally, are there _known_ fundamental limitations of algebraic
  15. > specifications?  Has anyone studied the "classes" of ADTs that can be
  16. > specified using various specification approaches?  If so, I would
  17. > appreciate a reference (or a short synopsis, if possible).
  18.  
  19. Some standard references on this topic are:
  20.  
  21.    J. Thatcher, E. Wagner and J. Wright.  Data type specification:
  22.    parameterization and the power of specification techniques.  ACM Trans. on
  23.    Programming Languages and Systems 4, 711-773 (1982).
  24.  
  25.    J. Bergstra, M. Broy, J. Tucker and M. Wirsing.  On the power of algebraic
  26.    specifications.  Proc. 1981 Symp. on Mathematical Foundations of Computer
  27.    Science.  Springer LNCS 118, 193-204 (1981).
  28.  
  29.    J. Bergstra and J. Tucker.  Initial and final algebra semantics: two
  30.    characterization theorems.  SIAM Journal on Computing 12(2), 366-387 (1983).
  31.  
  32.    J. Bergstra and J. Tucker.  Algebraic specifications of computable and
  33.    semicomputable data types.  Theoretical Computer Science 50, 137-181 (1987).
  34.  
  35. Briefly, there are different approaches to algebraic specification and
  36. the expressive power of a particular approach depends on whether or not it
  37. offers certain features.  One of the simplest approaches and the most classical
  38. is the so-called "initial algebra approach" via finite lists of equational
  39. axioms as described in:
  40.  
  41.    H. Ehrig and B. Mahr.  Fundamentals of Algebraic Specification 1. Equations
  42.    and Initial Semantics.  EATCS Monographs on Theoretical Computer Science.
  43.    Springer (1985).
  44.  
  45. This approach is not powerful enough to specify all recursive data structures
  46. (using "recursive" here in its recursion-theoretic sense).  Allowing hidden
  47. sorts and hidden functions makes this approach powerful enough to describe
  48. exactly all the semicomputable algebras.  Adding so-called "data constraints"
  49. or "hierarchy constraints" (or using a specification language in which the
  50. specification of new types of data cannot side-effect the interpretation of
  51. existing types, e.g. ASL) makes it possible to code universal and existential
  52. quantifiers over the natural numbers and so adds considerable expressive power,
  53. enough to allow the specification of any algebra you are likely to want (for
  54. the details of that vague statement see [BBTW81]).
  55.  
  56. A paper which explains some of the above and discusses its relevance to
  57. completeness of systems for proving theorems about specifications is:
  58.  
  59.    D. MacQueen and D. Sannella.  Completeness of proof systems for equational
  60.    specifications.  IEEE Trans. on Software Engineering SE-11(5), 454-461
  61.    (1985).
  62.  
  63. Of course, all of these expressiveness results are obtained via codings which,
  64. if used in practice, would make specifications difficult (if not impossible)
  65. to read.  Whether or not a particular data type can be *conveniently* specified
  66. is a different question.
  67.  
  68.  
  69. Don Sannella
  70. University of Edinburgh
  71.