LiquidHaskell
LiquidHaskell
复制标题
LiquidHaskell
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Ranjit Jhala
中科院分区：
文献类型：
--
作者：
Niki Vazou;Eric L. Seidel;Ranjit Jhala
Haskell具有许多令人愉快的功能。也许用户最受欢迎的是其类型系统，该系统允许开发人员在编译时指定和验证各种程序属性。但是，许多属性（通常取决于程序值之间的关系）是不可能的，或者至少是在现有类型系统中编码的繁琐属性。可以使用细化类型和外部SMT求解器的组合来验证许多此类属性。我们描述了精炼类型的Checker LiquidHaskell，我们用来指定和验证来自各种流行库的10,000行Haskell代码的各种属性，包括容器，Hscolour，hscolour，bytestring，text，vext，vector-algorithms and xmonad。首先，我们通过参观其功能介绍了LiquidHaskell的高级概述。其次，我们对可以检查的属性的种类进行定性讨论 - 从通用应用程序独立标准（如整体和终止）到应用程序的特定问题，例如内存安全性和数据结构正确性不变性。最后，我们对方法进行了定量评估，以期衡量验证所需的效率和程序员努力，并讨论方法的局限性。
Haskell has many delightful features. Perhaps the one most beloved by its users is its type system that allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within the existing type system. Many such properties can be verified using a combination of Refinement Types and external SMT solvers. We describe the refinement type checker liquidHaskell, which we have used to specify and verify a variety of properties of over 10,000 lines of Haskell code from various popular libraries, including containers, hscolour, bytestring, text, vector-algorithms and xmonad. First, we present a high-level overview of liquidHaskell, through a tour of its features. Second, we present a qualitative discussion of the kinds of properties that can be checked -- ranging from generic application independent criteria like totality and termination, to application specific concerns like memory safety and data structure correctness invariants. Finally, we present a quantitative evaluation of the approach, with a view towards measuring the efficiency and programmer effort required for verification, and discuss the limitations of the approach.