Some design principles and theory for OBJ-0, a language to express and execute algebraic specifications of programs | SpringerLink
Skip to main content
Springer Nature Link
Log in

Some design principles and theory for OBJ-0, a language to express and execute algebraic specifications of programs

  • Conference paper
  • First Online:
Mathematical Studies of Information Processing

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 75))

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. J.A. Goguen, J.W. Thatcher, E.G. Wagner and J.B. Wright. "Abstract data types as initial algebras and correctness of data representations." Proceedings, Conference on Computer Graphics, Pattern Recognition and Data Structure. (May 1975) pp. 89–93.

    Google Scholar 

  2. "Initial algebra semantics and continuous algebras." IBM Research Report RC-5701 (November 1975). Also, JACM 24 (1977) pp. 68–95.

    Google Scholar 

  3. E.A. Ashcroft, and W.W. Wadge, "LUCID — A Formal System for Writing and Proving Programs," SIAM Journal of Computing 5 (1976) pp. 336–354.

    Google Scholar 

  4. R.M. Burstall, "Design Considerations for a Functional Programming Language," to appear.

    Google Scholar 

  5. R.M. Burstall, and J. Darlington, "Some Transformations for Developing Recursive Programs," JACM 24 (1977), pp. 44–67.

    Google Scholar 

  6. R.M. Burstall, and J.A. Goguen, "Putting Theories Together to Make Specifications," Proceedings of Fifth International Joint Conference on Artificial Intelligence (August 1977) pp. 1045–1058.

    Google Scholar 

  7. P.M. Cohn, Universal Algebra Harper and Row (1965).

    Google Scholar 

  8. J.W. DeBakker, and W.P. DeRoever, "A Calculus for Recursive Program Schemes," Proceedings, International Conference on Automata, Languages, and Programs, Nivat, M., editor, North-Holland Publishing Co., Amsterdam, the Netherlands (1973) pp. 167–196.

    Google Scholar 

  9. R.W. Floyd, "Assigning Meanings to Programs," Proceedings, Symposium on Applied Math 19, American Mathematical Society, Providence, R.I. (1967) pp. 19–32.

    Google Scholar 

  10. J.A. Goguen, "Semantics of Computation", in Category Theory Applied to Computation and Control (ed E.G. Manes) Math and Computer Science Departments, University of Massachusetts at Amherst (1974) pp. 234–249; also Springer-Verlag, Lecture Notes in Computer Science, vol. 25 (1975) pp. 151–163.

    Google Scholar 

  11. J.A. Goguen, "Abstract Errors for Abstract Data Types," UCLA Semantics Theory of Computation Report #6, February 1977. Proceedings IFIP Working Conference on Formal Description of Programming Concepts. St. Andrews, New Brunswick (August 1977), pp. 21. 1–21. 32. Also, Formal Description of Programming Concepts (ed. E.J. Newhold) North Holland (1978) pp. 491–522.

    Google Scholar 

  12. J.A. Goguen, "Algebraic Specification," in New Directions in Software Technology (ed. P. Wegner) MIT Press (1978).

    Google Scholar 

  13. J.A. Goguen, and J. Tardo, "OBJ-0 Preliminary Users Manual," UCLA Semantics and Theory of Computation Report No. 10, (1977).

    Google Scholar 

  14. J.A. Goguen, J.W. Thatcher, and E.G. Wagner, "An initial algebra approach to the specification, correctness and implementation of abstract data types," IBM Research Report RC-6487 (October 1976). To appear in Current Trends in Programming Methodology, IV: Data Structuring (R. Yeh. Ed.) Prentice Hall. New Jersey (1978).

    Google Scholar 

  15. J.A. Goguen, J. Tardo, N. Williamson, and M. Zamfir, "A Practical Method for Testing Algebraic Specifications," to appear, UCLA Semantics and Theory of Computation Report (1978).

    Google Scholar 

  16. J.V. Guttag, "The Specification and Application to Programming of Abstract Data Types," University of Toronto, Computational Sciences Research Group, Report CSRG-59 (1975).

    Google Scholar 

  17. J.V. Guttag, "Abstract Data Types and the Development of Data Structures," Communications of the ACM, Vo. 20 (June 1977) pp. 397–404.

    Google Scholar 

  18. J.V. Guttag, E. Horowitz, and D.M. Musser, "Abstract Data Types and Software Validation, USC Information Sciences Institute, RR-76/48 (August 1976.).

    Google Scholar 

  19. J.V. Guttag, E. Horowitz, and D.M. Musser, "The Design of Data Type Specifications," USC Information Sciences Institute, RR-76/49 (November 1976). An expanded version of a paper which appeared in Proceedings of the Second International Conference on Software Engineering, San Francisco (October 1976).

    Google Scholar 

  20. D. Harm, "SCHEMER: An Initial Implementation," UCLA Artificial Intelligence Memo #8 (July 1977).

    Google Scholar 

  21. D. Harm, "An Abstract Specification of a Programming Language," UCLA Semantics and Theory of Computation, Report No. 11 (March 1978).

    Google Scholar 

  22. R. Haskell, and P.G. Harrison, "System Conventions for Non-procedural Languages," Publication 77/21, Department of Computing and Control, Imperial College, London (1977).

    Google Scholar 

  23. P. Henderson, and J. Morris, "A Lazy Evaluator," Third ACM Symposium on Principles of Programming Languages (1976) pp. 95–103.

    Google Scholar 

  24. C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Communications of the ACM 12 (1969) pp. 576–583.

    Google Scholar 

  25. G. Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems," IRIA — Report No. 250, Rocquencourt, France (1977).

    Google Scholar 

  26. T.M.S. Kaufman, "TED: A Text Editor Specified in OBJ," M.S.C. Essay, UCLA (1977).

    Google Scholar 

  27. D. Knuth, and P. Bendix, "Simple Word Prblems in Universal Algebra," in Computational Problems in Abstract Algebra, (J. Leech, editor) Pergammon Press, New York (1970), pp. 263–297.

    Google Scholar 

  28. D.S. Lankford, "Canonical Inference," University of Texas Automatic Theorem Proving Project Report ATP-32, (December 1975).

    Google Scholar 

  29. G. Levi, and F. Sirovich, "Proving Program Properties Symbolic Evaluation, and Logical Procedural Semantics," in Math Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 32, Springer-Verlag (1975) pp. 294–301.

    Google Scholar 

  30. B. Liskov and V. Berzins, "An Appraisal of Program Specification," MIT. Computational Structures Group, Memo 141–1 (1977); in New Directions in Software Technology (ed. P. Wegner), (1978).

    Google Scholar 

  31. Z. Manna, "Properites of Programs and the First Order Predicate Calculus," Journal of the ACM 16 (1969) pp. 244–255.

    Google Scholar 

  32. M.E. Majster, "Limits of the ‘Algebraic’ Specification of Abstract Data Types," SIGPLAN Notices 12 (October, 1977) pp. 37–42.

    Google Scholar 

  33. McCarthy, Levin et al(1965) J. McCarthy, P. Abrahams, D. Edwards, T. Hart, and M. Levin, LISP 1.5 Programmer's Manual, MIT Press, Cambridge, Massachusetts (1965).

    Google Scholar 

  34. M.A. Melkanoff, and M. Zamfir, "The Axiomatization of Data Base Conceptual Models by Abstract Data Types," Computer Science Department Report, UCLA-ENG-7785, UCLA (1978).

    Google Scholar 

  35. D.R. Musser, "A Data Type Verification System Based on Definite Rules," USC Information Sciences Institute, Marina del Rey, CA (1978).

    Google Scholar 

  36. M.J. O'Donnell, Computing in Systems Described by Equations, Lecture Notes in Computer Science, Vol. 58, Springer-Verlag (1977).

    Google Scholar 

  37. J.A. Robinson, "A Machine-Oriented Logic Based on the Resolution Principle," JACM 12 (1965) pp. 23–44.

    Google Scholar 

  38. B.A. Rosen, "Tree-Manipulating Systems and Church-Rosser Theorems," Journal of the ACM, Vol. 20 (January 1973) pp. 160–187.

    Google Scholar 

  39. J.W. Thatcher, E.G. Wagner, and J.B. Wright, "Specification of abstract data types using conditional axioms," IBM Research Report RC-6214 (September 1976).

    Google Scholar 

  40. J.W. Thatcher, E.G. Wagner, and J.B. Wright, "Data Type Specification: Parameterization and the Power of Specification Techniques," Proceedings, SIGACT 10th Annual Syposium on Theory of Computing (May, 1978) pp. 119–132.

    Google Scholar 

  41. M. Wand, "Algebraic Theories and Tree Rewriting Systems," Technical Report No. 66, Computer Science Department, Indiana University (July 1977).

    Google Scholar 

  42. M. Wand, "Compiling Lambda Expressions Using Continuations and Factorizations," Technical Report No. 55, Computer Science Department, Indiana University, (July 1977).

    Google Scholar 

  43. S. Zilles, "Abstract Specificational Data Types," Computation Structures Group Memo 119, MIT, Cambridge, MA (1974).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, UCLA, Los Angeles, California, USA

    Joseph A. Goguen

Authors
  1. Joseph A. Goguen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

E. K. Blum M. Paul S. Takasu

Rights and permissions

Reprints and permissions

Copyright information

© 1979 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goguen, J.A. (1979). Some design principles and theory for OBJ-0, a language to express and execute algebraic specifications of programs. In: Blum, E.K., Paul, M., Takasu, S. (eds) Mathematical Studies of Information Processing. Lecture Notes in Computer Science, vol 75. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09541-1_36

Download citation

  • DOI: https://doi.org/10.1007/3-540-09541-1_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-09541-5

  • Online ISBN: 978-3-540-35010-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation