Refinement types for Ruby

DOI10.1007/978-3-319-73721-8_13zbMATH Open1446.68032arXiv1711.09281OpenAlexW2768658963MaRDI QIDQ3296334FDOQ3296334

Authors: Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak 

Publication date: 7 July 2020

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1711.09281

Recommendations

• Refinement types for Haskell
• Gradual refinement types
• Abstract refinement types
• Refinement and retrenchment for programming language data types
• Language-based program verification via expressive types

zbMATH Keywords

refinement typesRubydynamic languagesRosette

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (1)

• Embedded domain specific verifiers

This page was built for publication: Refinement types for Ruby

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3296334)