Software Components as Invariant-Typed Arrows

(Keynote Talk)
  • Luis Soares Barbosa
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7554)


Invariants are constraints on software components which restrict their behavior in some desirable way, but whose maintenance entails some kind of proof obligation discharge. Such constraints may act not only over the input and output domains, as in a purely functional setting, but also over the underlying state space, as in the case of reactive components. This talk introduces an approach for reasoning about invariants which is both compositional and calculational: compositional because it is based on rules which break the complexity of such proof obligations across the structures involved; calculational because such rules are derived thanks to an algebra of invariants encoded in the language of binary relations. A main tool of this approach is the pointfree transform of the predicate calculus, which opens the possibility of changing the underlying mathematical space so as to enable agile algebraic calculation. The development of a theory of invariant preservation requires a broad, but uniform view of computational processes embodied in software components able to take into account data persistence and continued interaction. Such is the plan for this talk: we first introduce such processes as arrows, and then invariants as their types.


Binary Relation Software Component Computational Process Proof Obligation Business Rule 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Adámek, J.: Limits and colimits in generalized algebraic categories. Czechoslovak Mathematical Journal 26, 55–64 (1976)MathSciNetGoogle Scholar
  2. 2.
    Barbosa, L.S.: Towards a Calculus of State-based Software Components. Journal of Universal Computer Science 9(8), 891–909 (2003)Google Scholar
  3. 3.
    Barbosa, L.S., Oliveira, J.N.: Transposing partial components: an exercise on coalgebraic refinement. Theor. Comp. Sci. 365(1-2), 2–22 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Barbosa, L.S., Oliveira, J.N., Silva, A.: Calculating Invariants as Coreflexive Bisimulations. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 83–99. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Bird, R., Moor, O.: The Algebra of Programming. Series in Computer Science. Prentice Hall (1997)Google Scholar
  6. 6.
    Börger, E., Stärk, R.: Abstract state machines: A method for high-level system design and analysis. Springer (2003)Google Scholar
  7. 7.
    Hagino, T.: A Typed Lambda Calculus with Categorical Type Constructors. In: Pitt, D.H., Rydeheard, D.E., Poigné, A. (eds.) Category Theory and Computer Science. LNCS, vol. 283, pp. 140–157. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  8. 8.
    Meng, S., Barbosa, L.S.: Components as coalgebras: The refinement dimension. Theor. Comp. Sci. 351, 276–294 (2005)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Meng, S., Barbosa, L.S.: Towards the introduction of qos information in a component model. In: Shin, S.Y., Ossowski, S., Schumacher, M., Palakal, M.J., Hung, C.-C. (eds.) Proceedings of the 2010 ACM Symposium on Applied Computing, Sierre, Switzerland, pp. 2045–2046. ACM (2010)Google Scholar
  10. 10.
    Oliveira, J.N.: Extended Static Checking by Calculation Using the Pointfree Transform. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) LerNet 2008. LNCS, vol. 5520, pp. 195–251. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Poll, E., Zwanenburg, J.: From algebras and coalgebras to dialgebras. In: CMCS 2001. ENTCS, vol. 44, pp. 1–19. Elsevier (2001)Google Scholar
  12. 12.
    Reichel, H.: Unifying adt– and evolving algebra specifications. EATCS Bulletin 59, 112–126 (1996)zbMATHGoogle Scholar
  13. 13.
    Rutten, J.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 3–80 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Trnková, V., Goralcík, P.: On products in generalized algebraic categories. Commentationes Mathematicae Universitatis Carolinae 1, 49–89 (1972)Google Scholar
  15. 15.
    Trnková, V.: On descriptive classification of set-functors. I. Commentat. Math. Univ. Carol. 12, 143–174 (1971)zbMATHGoogle Scholar
  16. 16.
    Voutsadakis, G.: Universal dialgebra: Unifying universal algebra and coalgebra. Far East Journal of Mathematical Sciences 44(1) (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Luis Soares Barbosa
    • 1
  1. 1.HASLab - High Assurance Software LaboratoryINESC TEC & Universidade do MinhoPortugal

Personalised recommendations