Learning refinement types
Learning refinement types
复制标题
学习细化类型
DOI：
10.1145/2784731.2784766
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
S. Jagannathan
中科院分区：
文献类型：
--
作者：
He Zhu;A. Nori;S. Jagannathan
我们提出对于高阶函数程序，集成随机测试生成系统（能够发现程序错误）和细化类型系统（能够表达和验证程序不变量），并使用新颖的轻量级学习算法作为两者之间的有效中介。我们的方法基于众所周知的直觉，即有用但难以推断的程序属性通常可以从测试生成的具体程序状态中观察到；这些属性充当可能的不变量，如果用于细化简单类型，则可以通过细化类型检查器检查其有效性。我们描述了针对以 ML 编写的各种基准的技术实现，并证明了其在推断和证明表达复杂高阶控制和数据流的程序的有用不变量方面的有效性。
We propose the integration of a random test generation system (capable of discovering program bugs) and a refinement type system (capable of expressing and verifying program invariants), for higher-order functional programs, using a novel lightweight learning algorithm as an effective intermediary between the two. Our approach is based on the well-understood intuition that useful, but difficult to infer, program properties can often be observed from concrete program states generated by tests; these properties act as likely invariants, which if used to refine simple types, can have their validity checked by a refinement type checker. We describe an implementation of our technique for a variety of benchmarks written in ML, and demonstrate its effectiveness in inferring and proving useful invariants for programs that express complex higher-order control and dataflow.