Skip to main content
SpringerLink
Log in

Refinement Types for Ruby

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)

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

Abstract

Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification process. RTR works by encoding its verification problems into Rosette, a solver-aided host language. RTR handles mixins through assume-guarantee reasoning and uses just-in-time verification for metaprogramming. We formalize RTR by showing a translation from a core, Ruby-like language with refinement types into Rosette. We apply RTR to check a range of functional correctness properties on six Ruby programs. We find that RTR can successfully verify key methods in these programs, taking only a few minutes to perform verification.

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. Aggregate (2017). https://github.com/josephruscio/aggregate

  2. Boxroom (2017). https://github.com/mischa78/boxroom

  3. Businesstime (2017). https://github.com/bokmann/business_time/

  4. Geokit (2017). https://github.com/geokit/geokit

  5. Matrix (2017). https://github.com/ruby/matrix

  6. Money (2017). https://github.com/RubyMoney/money

  7. Unitwise (2017).https://github.com/joshwlewis/unitwise/

  8. Verified ruby apps (2017). https://raw.githubusercontent.com/mckaz/milod.kazerounian.github.io/master/static/VMCAI18/source.md

  9. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.Y.: A relational logic for higher-order programs (2017)

    Google Scholar 

  10. Ancona, D., Ancona, M., Cuni, A., Matsakis, N.D.: Rpython: A step towards reconciling dynamically and statically typed oo languages. In: DLS (2007)

    Google Scholar 

  11. Anderson, C., Giannini, P., Drossopoulou, S.: Towards type inference for JavaScript. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 428–452. Springer, Heidelberg (2005). https://doi.org/10.1007/11531142_19

    Chapter  Google Scholar 

  12. Aycock, J.: Aggressive type inference. In: International Python Conference (2000)

    Google Scholar 

  13. Bierman, G., Abadi, M., Torgersen, M.: Understanding TypeScript. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 257–281. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44202-9_11

    Google Scholar 

  14. Bocić, I., Bultan, T.: Symbolic model extraction for web application verification. In: ICSE (2017)

    Google Scholar 

  15. Chaudhuri, A., Foster, J.S.: Symbolic security analysis of ruby-on-rails web applications. In: CCS (2010)

    Google Scholar 

  16. Dean, J., Grove, D., Chambers, C.: Optimization of Object-Oriented Programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 77–101. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-49538-X_5

    Google Scholar 

  17. Foster, J., Ren, B., Strickland, S., Yu, A., Kazerounian, M.: RDL: Types, type checking, and contracts for Ruby (2017). https://github.com/plum-umd/rdl

  18. Freeman, T., Pfenning, F.: Refinement types for ML (1991)

    Google Scholar 

  19. Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: Jsketch: Sketching for java. In: ESEC/FSE 2015 (2015)

    Google Scholar 

  20. Jones, C.: Specification and design of (parallel) programs. In: IFIP Congress (1983)

    Google Scholar 

  21. Kent, A.M., Kempe, D., Tobin-Hochstadt, S.: Occurrence typing modulo theories. In: PLDI (2016)

    Google Scholar 

  22. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  Google Scholar 

  23. Lerner, B.S., Politz, J.G., Guha, A., Krishnamurthi, S.: Tejas: Retrofitting type systems for JavaScript (2013)

    Google Scholar 

  24. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  25. Near, J.P., Jackson, D.: Rubicon: Bounded verification of web applications. In: FSE 2012 (2012)

    Google Scholar 

  26. Near, J.P., Jackson, D.: Finding security bugs in web applications using a catalog of access control patterns. In: ICSE 2016 (2016)

    Google Scholar 

  27. Pernsteiner, S., Loncaric, C., Torlak, E., Tatlock, Z., Wang, X., Ernst, M.D., Jacky, J.: Investigating safety of a radiotherapy machine using system models with pluggable checkers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 23–41. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_2

    Google Scholar 

  28. Protzenko, J., Zinzindohoué, J.K., Rastogi, A., Ramananandro, T., Wang, P., Zanella-Béguelin, S., Delignat-Lavaud, A., Hriţcu, C., Bhargavan, K., Fournet, C., Swamy, N.: Verified low-level programming embedded in f* (2017)

    Google Scholar 

  29. Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for TypeScript (2015)

    Google Scholar 

  30. Ren, B.M., Foster, J.S.: Just-in-time static type checking for dynamic languages. In: PLDI (2016)

    Google Scholar 

  31. Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI (2008)

    Google Scholar 

  32. Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in pvs. IEEE Trans. Softw., Eng. (1998)

    Google Scholar 

  33. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LFP 1992 (1992)

    Google Scholar 

  34. Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: PLDI (2013)

    Google Scholar 

  35. Thiemann, P.: Towards a type system for analyzing JavaScript programs. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 408–422. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_28

    Chapter  Google Scholar 

  36. Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: From scripts to programs. In: OOPSLA (2006)

    Google Scholar 

  37. Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: POPL (2008)

    Google Scholar 

  38. Torlak, E., Bodik, R.: Growing solver-aided languages with rosette. Onward! (2013)

    Google Scholar 

  39. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell (2014)

    Google Scholar 

  40. Vekris, P., Cosman, B., Jhala, R.: Refinement types for TypeScript (2016)

    Google Scholar 

  41. Vytiniotis, D., Peyton Jones, S., Claessen, K., Rosén, D.: Halo: Haskell to logic through denotational semantics. In: POPL (2013)

    Google Scholar 

  42. Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: OOPSLA (2016)

    Google Scholar 

  43. Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Maryland, College Park, USA

    Milod Kazerounian, Niki Vazou, Austin Bourgerie & Jeffrey S. Foster

  2. University of Washington, Seattle, USA

    Emina Torlak

Authors
  1. Milod Kazerounian
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Niki Vazou
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Austin Bourgerie
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jeffrey S. Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Emina Torlak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Milod Kazerounian .

Editor information

Editors and Affiliations

  1. University of Texas , Austin, Texas, USA

    Isil Dillig

  2. University of California , Los Angeles, California, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kazerounian, M., Vazou, N., Bourgerie, A., Foster, J.S., Torlak, E. (2018). Refinement Types for Ruby. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-73721-8_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-73720-1

  • Online ISBN: 978-3-319-73721-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation