Refinement type checking via assertion checking

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

研究成果: ジャーナルへの寄稿記事

1 引用 (Scopus)

抄録

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.

元の言語英語
ページ(範囲)827-834
ページ数8
ジャーナルJournal of Information Processing
23
発行部数6
DOI
出版物ステータス出版済み - 1 1 2015
外部発表Yes

Fingerprint

Specifications
Experiments

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

これを引用

Refinement type checking via assertion checking. / Sato, Ryosuke; Asada, Kazuyuki; Kobayashi, Naoki.

:: Journal of Information Processing, 巻 23, 番号 6, 01.01.2015, p. 827-834.

研究成果: ジャーナルへの寄稿記事

Sato, Ryosuke ; Asada, Kazuyuki ; Kobayashi, Naoki. / Refinement type checking via assertion checking. :: Journal of Information Processing. 2015 ; 巻 23, 番号 6. pp. 827-834.
@article{3f22bffa2a75467c88d28b8f1c44a59b,
title = "Refinement type checking via assertion checking",
abstract = "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.",
author = "Ryosuke Sato and Kazuyuki Asada and Naoki Kobayashi",
year = "2015",
month = "1",
day = "1",
doi = "10.2197/ipsjjip.23.827",
language = "English",
volume = "23",
pages = "827--834",
journal = "Journal of Information Processing",
issn = "0387-6101",
publisher = "Information Processing Society of Japan",
number = "6",

}

TY - JOUR

T1 - Refinement type checking via assertion checking

AU - Sato, Ryosuke

AU - Asada, Kazuyuki

AU - Kobayashi, Naoki

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84947233320&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947233320&partnerID=8YFLogxK

U2 - 10.2197/ipsjjip.23.827

DO - 10.2197/ipsjjip.23.827

M3 - Article

VL - 23

SP - 827

EP - 834

JO - Journal of Information Processing

JF - Journal of Information Processing

SN - 0387-6101

IS - 6

ER -