A logical approach to data structures

ABSTRACT

The Galois project at the University of Texas is building a programming environment that supports the formal development and verification of data structure programs. This programming environment supports features such as pointer manipulation and destructive update that often make formal treatment difficult.

REFERENCES

• 1: Beeri, Catriel, et al, Embedding Y-terms in a Hornclause Logic Language, MCC Technical Report, ACA-ST-050-88
• 2: Berg, H. K., et al, Formal Methods of Program Verification and Spe@ication, Prentice-Hall, 1982
• 3: Boyer, Robert S. and Moore, J. Struther, A Computational Logic, Academic Press, 1979
• 4: W F. Clocksin , Christopher S. Mellish, Programming in Prolog (2nd ed.), Springer-Verlag New York, Inc., New York, NY, 1984
• 5: Ershov, A. P., Axiomatic for Memory Allocation, Acts Informatica, v. 6 n, 1, 1976
• 6: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 7: Guttag, J. V., and Horning, J. J., The Algebraic Specification of Abstract Data Types
• 8: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 9: Kumar, Mohan, A Compiler for Galois, Master's Thesis, University of Texas at Austin, 1992
• 10: William Leler, Constraint programming languages: their specification and generation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 11: David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
• 12: Maier, D., A Logic for Objects, in Proc of the Workshop on the Foundations of Deductive Databases and Logic Programming, Washington DC, August 1986, pp. 6-26
• 13: Frank G. Pagen, Formal Specifications of Programming Language: A Panoramic Primer, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 14: Ray, Patrick, Programming in Galois, forthcoming Master's thesis, University of Texas at Austin
• 15: W. Richard Stark, LISP, lore, and logic: an algebraic view of LISP programming, foundations, and applications, Springer-Verlag New York, Inc., New York, NY, 1990
• 16: William Russell Turpin, Programming data structures in logic, University of Texas at Austin, Austin, TX, 1992

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

General Terms:
Design, Theory, Verification