Skip to main content
SpringerLink
Log in

A Type System for Usage of Software Components

  • Conference paper
Types for Proofs and Programs (TYPES 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5497))

Included in the following conference series:

  • 291 Accesses

Abstract

The aim of this article is to support component-based software engineering by modelling exclusive and inclusive usage of software components. Truong and Bezem describe in several papers abstract languages for component software with the aim to find bounds of the number of instances of components. Their language includes primitives for instantiating and deleting instances of components and operators for sequential, alternative and parallel composition and a scope mechanism. The language is here supplemented with the primitives use, lock and free. The main contribution is a type system which guarantees the safety of usage, in the following way: When a well-typed program executes a subexpression use[x] or lock[x], it is guaranteed that an instance of x is available.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. McIlroy, M.D.: Mass produced software components. In: Naur, P., Randell, B. (eds.) Software Engineering: Report of a conference sponsored by the NATO Science Committee, pp. 79–87. Scientific Affairs Division, NATO (1968)

    Google Scholar 

  2. Szyperski, C.: Component Software—Beyond Object–Oriented Programming, 2nd edn. Addison–Wesley / ACM Press (2002)

    Google Scholar 

  3. Bezem, M., Truong, H.: A type system for the safe instantiation of components. Electronic Notes in Theoretical Computer Science 97, 197–217 (2004)

    Article  Google Scholar 

  4. Truong, H.: Guaranteeing resource bounds for component software. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 179–194. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Truong, H., Bezem, M.: Finding resource bounds in the presence of explicit deallocation. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 227–241. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Book  MATH  Google Scholar 

  7. Bezem, M., Hovland, D., Truong, H.: A type system for counting instances of software components. Technical Report 363, Department of Informatics, The University of Bergen, P.O. Box 7800, N-5020 Bergen, Norway (2007)

    Google Scholar 

  8. Stroustrup, B.: The C++ Programming Language, Third Edition. Addison-Wesley, Reading (2000)

    MATH  Google Scholar 

  9. IEEE: The open group base specifications issue 6 (2004)

    Google Scholar 

  10. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  11. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  12. Crary, K., Weirich, S.: Resource bound certification. In: POPL 2000: Proceedings of the 27th ACM SIGPLAN–SIGACT symposium on Principles of programming languages, pp. 184–198. ACM Press, New York (2000)

    Google Scholar 

  13. Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: POPL 2003: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 185–197. ACM Press, New York (2003)

    Google Scholar 

  14. Kobayashi, N., Suenaga, K., Wischik, L.: Resource usage analysis for the π-calculus. Logical Methods in Computer Science 2(3) (2006)

    Google Scholar 

  15. Unnikrishnan, L., Stoller, S.D., Liu, Y.A.: Optimized live heap bound analysis. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 70–85. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Popeea, C., Chin, W.N.: A type system for resource protocol verification and its correctness proof. In: Heintze, N., Sestoft, P. (eds.) PEPM, pp. 135–146. ACM, New York (2004)

    Google Scholar 

  17. Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Trans. Program. Lang. Syst. 27(2), 264–313 (2005)

    Article  MATH  Google Scholar 

  18. Braberman, V., Garbervetsky, D., Yovine, S.: A static analysis for synthesizing parametric specifications of dynamic memory consumption. Journal of Object Technology 5(5), 31–58 (2006)

    Article  Google Scholar 

  19. Chin, W.N., Nguyen, H.H., Qin, S., Rinard, M.C.: Memory usage verification for OO programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 70–86. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Hofmann, M., Jost, S.: Type-based amortised heap-space analysis (for an object-oriented language). In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: OOPSLA, pp. 211–230 (2002)

    Google Scholar 

  22. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, The University of Bergen, PB 7803, N-5020, Bergen, Norway

    Dag Hovland

Authors
  1. Dag Hovland
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Stefano Berardi  & Ugo de’Liguoro  & 

  2. Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Ferruccio Damiani

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hovland, D. (2009). A Type System for Usage of Software Components. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds) Types for Proofs and Programs. TYPES 2008. Lecture Notes in Computer Science, vol 5497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02444-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02444-3_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02443-6

  • Online ISBN: 978-3-642-02444-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation