Advertisement

Order-Sorted Parameterization and Induction

  • José Meseguer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5700)

Abstract

Parameterization is one of the most powerful features to make specifications and declarative programs modular and reusable, and our best hope for scaling up formal verification efforts. This paper studies order-sorted parameterization at three different levels: (i) its mathematical semantics; (ii) its operational semantics by term rewriting; and (iii) the inductive reasoning principles that can soundly be used to prove properties about such specifications. It shows that achieving the desired properties at each of these three levels is a considerably subtler matter than for many-sorted specifications, but that such properties can be attained under reasonable conditions.

Keywords

Operational Semantic Critical Pair Forgetful Functor Signature Morphism Initial Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bénabou, J.: Structures algébriques dans les catégories. Cahiers de Topologie et Géometrie Différentielle 10, 1–126 (1968)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sannella, D. (eds.): Algebraic System Specification and Development. LNCS, vol. 501. Springer, Heidelberg (1991)zbMATHGoogle Scholar
  3. 3.
    Bidoit, M., Mosses, P.D. (eds.): CASL User Manual. LNCS, vol. 2900. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  4. 4.
    Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theor. Comput. Sci. 170(1-2), 245–276 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bouhoula, A., Jouannaud, J.-P.: Automata-driven automated induction. Inf. Comput. 169(1), 1–22 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science 236, 35–132 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Burstall, R., Goguen, J.: Putting theories together to make specifications. In: Reddy, R. (ed.) Proceedings, Fifth International Joint Conference on Artificial Intelligence, pp. 1045–1058. Department of Computer Science, Carnegie-Mellon University (1977)Google Scholar
  8. 8.
    Burstall, R., Goguen, J.A.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  9. 9.
    Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. CSLI Publications (2000)Google Scholar
  10. 10.
    Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Amsterdam (2000), http://maude.cs.uiuc.edu Google Scholar
  11. 11.
    Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  12. 12.
    Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), http://www.grappa.univ-lille3.fr/tata (Release, October 12th 2007)
  13. 13.
    Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Cambridge UP, Cambridge (1993)Google Scholar
  14. 14.
    Ehrich, H.-D.: On the theory of specification, implementation, and parametrization of abstract data types. J. ACM 29(1), 206–227 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Ehrig, H., Kreowski, H.-J., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Parameter passing in algebraic specification languages. Theor. Comput. Sci. 28, 45–81 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification, vol. 1. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  17. 17.
    Futatsugi, K.: Verifying specifications with proof scores in CafeOBJ. In: ASE 2006, 21st IEEE/ACM International Conference on Automated Software Engineering, pp. 3–10 (2006)Google Scholar
  18. 18.
    Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series (1998)Google Scholar
  19. 19.
    Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Reid, B. (ed.) Proceedings of 12th ACM Symposium on Principles of Programming Languages, pp. 52–66. ACM Press, New York (1985)Google Scholar
  20. 20.
    Ganzinger, H.: Parameterized specifications: Parameter passing and implementation with respect to observability. ACM Trans. Program. Lang. Syst. 5(3), 318–354 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Goguen, J.: OBJ as a theorem prover with application to hardware verification. In: Subramanyam, P., Birtwistle, G. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 218–267. Springer, Heidelberg (1989)Google Scholar
  22. 22.
    Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Goguen, J., Meseguer, J.: Universal realization, persistent interconnection and implementation of abstract modules. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 265–281. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  24. 24.
    Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Levi, G., Montanari, U. (eds.) TAPSOFT 1987 and CFLP 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987)Google Scholar
  25. 25.
    Goguen, J., Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105, 217–273 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer Academic Publishers, Dordrecht (2000)CrossRefGoogle Scholar
  27. 27.
    Haxthausen, A.E., Nickl, F.: Pushouts of order-sorted algebraic specifications. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 132–147. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  28. 28.
    Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  29. 29.
    Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electr. Notes Theor. Comput. Sci (2008); To appear in Proc. of RULE 2008Google Scholar
  30. 30.
    Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  31. 31.
    Hendrix, J.D.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign, UIUCDCS-R-2008-2999 (2008), http://www.cs.uiuc.edu/research/phdtheses.php
  32. 32.
    Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)Google Scholar
  33. 33.
    Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepistö, T., Salomaa, A. (eds.) ICALP 1988. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  34. 34.
    Kirchner, H.: Proofs in parameterized specifications. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 174–187. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  35. 35.
    Lawvere, F.W.: Functorial semantics of algebraic theories. Proceedings National Academy of Sciences 50, 869–873 (1963); Summary of Ph.D. Thesis, Columbia UniversityMathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    MacLane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)zbMATHGoogle Scholar
  37. 37.
    Meseguer, J.: General logics. In: Logic Colloquium 1987, pp. 275–329. North-Holland, Amsterdam (1989)Google Scholar
  38. 38.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  39. 39.
    Meseguer, J., Goguen, J., Smolka, G.: Order-sorted unification. J. Symbolic Computation 8, 383–413 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Mosses, P.: Action Semantics. Cambridge University Press, Cambridge (1992)CrossRefzbMATHGoogle Scholar
  41. 41.
    Mosses, P.D.: A basic abstract semantic algebra. In: Plotkin, G., MacQueen, D.B., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 87–107. Springer, Heidelberg (1984)CrossRefGoogle Scholar
  42. 42.
    Mosses, P.D.: Unified algebras and action semantics. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol. 349, pp. 17–35. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  43. 43.
    Mosses, P.D.: Unified algebras and institutions. In: Proc. Fourth Annual IEEE Symp. on Logic in Computer Science, Asilomar, California, June 1989, pp. 304–312 (1989)Google Scholar
  44. 44.
    Mosses, P.D.: Unified algebras and modules. In: POPL, pp. 329–343 (1989)Google Scholar
  45. 45.
    Mosses, P.D.: The use of sorts in algebraic specifications. In: Bidoit, M., Choppy, C. (eds.) COMPASS/ADT 1991. LNCS, vol. 655, pp. 66–92. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  46. 46.
    Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  47. 47.
    Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program. 60-61, 195–228 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Padawitz, P.: Parameter-preserving data type specifications. J. Comput. Syst. Sci. 34(2/3), 179–209 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  49. 49.
    Padawitz, P.: The equational theory of parameterized specifications. Inf. Comput. 76(2/3), 121–137 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  50. 50.
    Poigné, A.: Parametrization for order-sorted algebraic specification. J. Comput. Syst. Sci. 40(2), 229–268 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    Qian, Z.: Another look at parameterization for order-sorted algebraic specifications. J. Comput. Syst. Sci. 49(3), 620–666 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  52. 52.
    Schröder, L., Mossakowski, T., Tarlecki, A., Klin, B., Hoffman, P.: Amalgamation in the semantics of CASL. Theor. Comput. Sci. 331(1), 215–247 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Smolka, G., Nutt, W., Goguen, J., Meseguer, J.: Order-sorted equational computation. In: Nivat, M., Aït-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, vol. 2, pp. 297–367. Academic Press, London (1989)Google Scholar
  54. 54.
    Strachey, C., Milne, R.: A Theory of Programming Language Semantics. Chapman and Hall, Boca Raton (1976)zbMATHGoogle Scholar
  55. 55.
    Thatcher, J.W., Wagner, E.G., Wright, J.B.: Data type specification: Parameterization and the power of specification techniques. In: STOC 1978 Tenth Annual ACM Symposium on Theory of Computing, pp. 119–132. ACM Press, New York (1978)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • José Meseguer
    • 1
  1. 1.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations