2026-04-17T16:02:15Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00145136 2025-01-20T06:42:51Z 934:935:8226:8284

Refinement Type Checking via Assertion Checking Refinement Type Checking via Assertion Checking Ryosuke, Sato Kazuyuki, Asada Naoki, Kobayashi Ryosuke, Sato Kazuyuki, Asada Naoki, Kobayashi [通常論文] refinement types, assertion checking, automated verification A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments. \n------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.23(2015) No.6(online) ------------------------------ A refinement type can be used to express a detailed specification of a higher-order functional program. Given a refinement type as a specification of a program, we can verify that the program satisfies the specification by checking that the program has the refinement type. Refinement type checking/inference has been extensively studied and a number of refinement type checkers have been implemented. Most of the existing refinement type checkers, however, need type annotations, which is a heavy burden on users. To overcome this problem, we reduce a refinement type checking problem to an assertion checking problem, which asks whether the assertions in a program never fail; and then we use an existing assertion checker to solve it. This reduction enables us to construct a fully automated refinement type checker by using a state-of-the-art fully automated assertion checker. We also prove the soundness and the completeness of the reduction, and report on implementation and preliminary experiments. \n------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.23(2015) No.6(online) ------------------------------ 情報処理学会 2015-09-21 eng journal article https://ipsj.ixsq.nii.ac.jp/records/145136 1882-7802 AA11464814 情報処理学会論文誌プログラミング（PRO） 8 3 https://ipsj.ixsq.nii.ac.jp/record/145136/files/IPSJ-TPRO0803002.pdf application/pdf 388.9 kB 2017-09-21