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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aggregate (2017). https://github.com/josephruscio/aggregate
Boxroom (2017). https://github.com/mischa78/boxroom
Businesstime (2017). https://github.com/bokmann/business_time/
Geokit (2017). https://github.com/geokit/geokit
Matrix (2017). https://github.com/ruby/matrix
Money (2017). https://github.com/RubyMoney/money
Unitwise (2017).https://github.com/joshwlewis/unitwise/
Verified ruby apps (2017). https://raw.githubusercontent.com/mckaz/milod.kazerounian.github.io/master/static/VMCAI18/source.md
Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.Y.: A relational logic for higher-order programs (2017)
Ancona, D., Ancona, M., Cuni, A., Matsakis, N.D.: Rpython: A step towards reconciling dynamically and statically typed oo languages. In: DLS (2007)
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
Aycock, J.: Aggressive type inference. In: International Python Conference (2000)
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
Bocić, I., Bultan, T.: Symbolic model extraction for web application verification. In: ICSE (2017)
Chaudhuri, A., Foster, J.S.: Symbolic security analysis of ruby-on-rails web applications. In: CCS (2010)
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
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
Freeman, T., Pfenning, F.: Refinement types for ML (1991)
Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: Jsketch: Sketching for java. In: ESEC/FSE 2015 (2015)
Jones, C.: Specification and design of (parallel) programs. In: IFIP Congress (1983)
Kent, A.M., Kempe, D., Tobin-Hochstadt, S.: Occurrence typing modulo theories. In: PLDI (2016)
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
Lerner, B.S., Politz, J.G., Guha, A., Krishnamurthi, S.: Tejas: Retrofitting type systems for JavaScript (2013)
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
Near, J.P., Jackson, D.: Rubicon: Bounded verification of web applications. In: FSE 2012 (2012)
Near, J.P., Jackson, D.: Finding security bugs in web applications using a catalog of access control patterns. In: ICSE 2016 (2016)
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
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)
Rastogi, A., Swamy, N., Fournet, C., Bierman, G., Vekris, P.: Safe & efficient gradual typing for TypeScript (2015)
Ren, B.M., Foster, J.S.: Just-in-time static type checking for dynamic languages. In: PLDI (2016)
Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI (2008)
Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in pvs. IEEE Trans. Softw., Eng. (1998)
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LFP 1992 (1992)
Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: PLDI (2013)
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
Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: From scripts to programs. In: OOPSLA (2006)
Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: POPL (2008)
Torlak, E., Bodik, R.: Growing solver-aided languages with rosette. Onward! (2013)
Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for haskell (2014)
Vekris, P., Cosman, B., Jhala, R.: Refinement types for TypeScript (2016)
Vytiniotis, D., Peyton Jones, S., Claessen, K., Rosén, D.: Halo: Haskell to logic through denotational semantics. In: POPL (2013)
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)
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
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)