Refinement of Parameterized Algebraic Specifications

  • Yellamraju V. Srinivas
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


A refinement relation for parameterized algebraic specifications is introduced in which the body specification is refined covariantly (i.e., specialized) while the parameter specification is refined contravariantly (i.e., generalized). This refinement is similar to the subtyping relation between function types. Assuming a few relatively weak axioms about parameterized specifications, refinement is shown to satisfy the expected properties for software development in-the-large: independent refinement of body and parameter, and closure under sequential composition, instantiation and a suitable form of ‘horizontal’ composition.


Parameterized specifications mixed-variance refinement compositionality 


  1. Bidoit, M. (1987), The stratified loose approach: A generalization of initial and loose semantics, in ‘Recent Trends in Data Type Specification’, Vol. 332 of Lecture Notes in Computer Science, Springer-Verlag, Gullane, Scotland, pp. 1–22.Google Scholar
  2. Burstall, R. M. & Goguen, J. A. (1977), Putting theories together to make specifications, in ‘Proc. 5th Int. Joint Conf. on Artificial Intelligence’, pp. 1045–1058.Google Scholar
  3. Ehrig, H. & Große-Rhode, M. (1994), ‘Functorial theory of parameterized specifications in a general specification framework’, Theoretical Computer Science 135, 221–266.zbMATHMathSciNetCrossRefGoogle Scholar
  4. Ehrig, H. & Kreowski, H. J. (1982), Parameter passing commutes with implementation of parameterized data types, in ‘9thICALP’, Vol. 140 of Lecture Notes in Computer Science, Springer-Verlag, Aarhus, Denmark, pp. 197–211.Google Scholar
  5. Ehrig, H., Kreowski, H. J., Thatcher, J., Wagner, E. & Wright, J. (1981), Parameter passing in algebraic specification languages, in ‘Proceedings, Workshop on Program Specification’, Vol. 134 of Lecture Notes in Computer Science, Springer-Verlag, Aarhus, Denmark, pp. 322–369.Google Scholar
  6. Ehrig, H. & Mahr, B. (1990), Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, Vol. 21 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, Berlin.zbMATHCrossRefGoogle Scholar
  7. Ganzinger, H. (1983), ‘Parameterized specifications: Parameter passing and implementation with respect to observability’, ACM Transactions on Programming Languages and Systems 5 (3), 318–354.zbMATHCrossRefGoogle Scholar
  8. Goguen, J. A. & Meseguer, J. (1982), Universal realization, persistent interconnection and implementation of abstract modules, in ‘9thICALP’, Vol. 140 of Lecture Notes in Computer Science, Springer-Verlag, Aarhus, Denmark, pp. 265–281.Google Scholar
  9. Lambek, J. & Scott, P. J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge.zbMATHGoogle Scholar
  10. Sannella, D. & Tarlecki, A. (1988), ‘Towards formal development of programs from algebraic specifications: Implementations revisited’, Acta Informatica 25, 233–281.zbMATHMathSciNetCrossRefGoogle Scholar
  11. Sannella, D. & Wirsing, M. (1982), Implementation of parameterized specifications, in ‘9thICALP’, Vol. 140 of Lecture Notes in Computer Science, Springer-Verlag, Aarhus, Denmark, pp. 473–488. Extended abstract.Google Scholar
  12. Srinivas, Y. V. & Jüllig, R. (1995), Specware:tm formal support for composing software, in B. Moeller, ed., ‘Proceedings of the Conference on Mathematics of Program Construction’, Springer-Verlag, Berlin, pp. 399–422. Lecture Notes in Computer Science, Vol. 947.CrossRefGoogle Scholar
  13. Wirsing, M. (1986), ‘Structured algebraic specifications: A kernel language’, Theoretical Computer Science 42, 123–249.zbMATHMathSciNetCrossRefGoogle Scholar

Copyright information

© IFIP 1997

Authors and Affiliations

  • Yellamraju V. Srinivas
    • 1
  1. 1.Kestrel InstitutePalo AltoUSA

Personalised recommendations