Ruby 的精化类型
编程语言
2017-11-28 v1
摘要
精化类型（refinement types）是一种流行的用于指定和推理关键程序属性的方法。本文介绍 RTR，一个为 Ruby 添加精化类型的新系统。RTR 构建于 RDL 之上，RDL 是一个为验证过程提供基本类型信息的 Ruby 类型检查器。RTR 通过将其验证问题编码到 Rosette（一种求解器辅助的主语言）中工作。RTR 通过假设-保证推理处理 mixin，并对元编程使用即时验证。我们通过展示从带有精化类型的类 Ruby 核心语言到 Rosette 的翻译来形式化 RTR。我们将 RTR 应用于检查六个 Ruby 程序上的一系列功能正确性属性。我们发现 RTR 能够成功验证这些程序中的关键方法，仅花费几分钟即可完成验证。
引用
@article{arxiv.1711.09281,
title = {Refinement Types for Ruby},
author = {Milod Kazerounian and Niki Vazou and Austin Bourgerie and Jeffrey S. Foster and Emina Torlak},
journal= {arXiv preprint arXiv:1711.09281},
year = {2017}
}