Skip to main content
SpringerLink
Log in

Refinement Types for tla  + 

  • Conference paper
NASA Formal Methods (NFM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8430))

Included in the following conference series:

Abstract

tla  +  is a specification language, mainly intended for concurrent and distributed systems. Its non-temporal fragment is based on a variant of (untyped) zf set theory. Motivated by the integration of the tla  +  Proof System with smt solvers or similar tools based on multi-sorted first-order logic, we define a type system for tla  +  and we prove its soundness. The system includes refinement types, which fit naturally in set theory. Combined with dependent function types, we obtain type annotations on top of an untyped specification language, getting the best of both the typed and untyped approaches. After implementing the type inference algorithm, we show that the resulting typing discipline improves the verification capabilities of the proof system.

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. Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)

    Google Scholar 

  2. Aspinall, D., Compagnoni, A.B.: Subtyping dependent types. Theor. Comput. Sci. 266(1-2), 273–309 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: Cvc4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), www.SMT-LIB.org

  5. Déharbe, D.: Integration of SMT-solvers in B and Event-B development environments. Sci. Comput. Program. 78(3), 310–326 (2013)

    Article  MATH  Google Scholar 

  6. Dowek, G.: Collections, sets and types. Mathematical. Structures in Comp. Sci. 9(1), 109–123 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  7. Freeman, T., Pfenning, F.: Refinement types for ML. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, PLDI 1991, pp. 268–277. ACM, New York (1991)

    Chapter  Google Scholar 

  8. Heeren, B., Hage, J., Swierstra, D.: Generalizing Hindley-Milner type inference algorithms. Technical report (2002)

    Google Scholar 

  9. Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321 (1991)

    Google Scholar 

  10. Knowles, K., Flanagan, C.: Type reconstruction for general refinement types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 505–519. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Lamport, L.: Specifying Systems: The TLA +  Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston, Mass (2002)

    Google Scholar 

  12. Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Trans. Program. Lang. Syst. 21(3), 502–526 (1999)

    Article  Google Scholar 

  13. Manzano, M.: Extensions of First-Order Logic, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2005)

    Google Scholar 

  14. Merz, S., Vanzetto, H.: Harnessing SMT Solvers for Tla  +  Proofs. ECEASST, 53 (2012)

    Google Scholar 

  15. Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. In: Fourth International Workshop on Foundations of Object-Oriented Programming, FOOL (1997)

    Google Scholar 

  16. Pottier, F.: Simplifying subtyping constraints. In: Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, pp. 122–133. ACM Press (1996)

    Google Scholar 

  17. Pottier, F., Rémy, D.: The essence of ML type inference. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, ch. 10, pp. 389–489. MIT Press (2005)

    Google Scholar 

  18. Rushby, J., Owre, S., Shankar, N.: Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (1998)

    Article  Google Scholar 

  19. Spivey, M.: The Z Notation: A Reference Manual. Prentice Hall (1992)

    Google Scholar 

  20. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Appel, A.W., Aiken, A. (eds.) POPL, pp. 214–227. ACM (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, Villers-lès-Nancy, France

    Stephan Merz & Hernán Vanzetto

  2. LORIA, France

    Stephan Merz & Hernán Vanzetto

  3. Microsoft Research-INRIA Joint Centre, Saclay, France

    Hernán Vanzetto

Authors
  1. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hernán Vanzetto
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA, 2101 NASA Parkway, M/C ER4, 77058, Houston, TX, USA

    Julia M. Badger

  2. Intelligent Systems Division, NASA Ames Research Center, 94035, Moffett Field, CA, USA

    Kristin Yvonne Rozier

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Merz, S., Vanzetto, H. (2014). Refinement Types for tla  +  . In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-06200-6_11

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-06199-3

  • Online ISBN: 978-3-319-06200-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation