ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
- PDF / 1,065,895 Bytes
- 26 Pages / 439.37 x 666.142 pts Page_size
- 102 Downloads / 192 Views
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs Adrien Champion1,2 · Tomoya Chiba3 · Naoki Kobayashi3
· Ryosuke Sato4
Received: 18 June 2020 / Accepted: 26 June 2020 © Springer Nature B.V. 2020
Abstract We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework uses implication constraints, which consist of pairs (x, y) such that if x satisfies an invariant, so does y. From these constraints, Ice infers inductive invariants effectively. We observe that the implication constraints in the original Ice framework are not suitable for finding invariants of recursive functions with multiple function calls. We thus generalize the implication constraints to those of the form ({x1 , . . . , xk }, y), which means that if all of x1 , . . . , xk satisfy an invariant, so does y. We extend their algorithms for inferring likely invariants from samples, verifying the inferred invariants, and generating new samples. We have implemented our method and confirmed its effectiveness through experiments. Keywords Higher-order program verification · Machine learning · Formal verification · Refinement types
B
Naoki Kobayashi [email protected] Adrien Champion [email protected] Tomoya Chiba [email protected] Ryosuke Sato [email protected]
1
The University of Tokyo, Tokyo, Japan
2
Present Address: OCamlPro, Paris, France
3
The University of Tokyo, Tokyo, Japan
4
Kyushu University, Fukuoka, Japan
123
A. Champion et al.
1 Introduction Higher-order functional program verification is an interesting and challenging problem. Over the past two decades, several approaches have been proposed: refinement types with manual annotations [12,33], liquid types [24], and reduction to higher-order recursion schemes [26]. These approaches face the same problem found in imperative and synchronous data-flow program verification: the need for predicates describing how loops and components behave for the verification and/or abstraction method to work in practice [8,14,19]. This paper proposes to address this issue by combining refinement types with the recent machine-learning-based, invariant discovery framework Ice from [13,14]. Consider for instance a function f from integers to integers such that if its input n is less than or equal to 101, then its output is 91, otherwise it is n − 10. (This is the case of the mc_91 function on Fig. 1.) Then our objective is to automatically discover, by using an adaptation of Ice, the refinement type f : {n : int | true} → {r : int | (n > 101 ∧ r = n − 10) ∨ r = 91}. That is, function f accepts any integer n that satisfies true as input, and yields an integer r equal to n − 10 when n > 101, and equal to 91 otherwise. The traditional Ice framework is not appropriate for our use-case. We briefly summarize it below, and then discuss how this appr
Data Loading...
