研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	2003
形態種別	学術雑誌
査読	査読あり
標題	Combining Testing and Proving in Dependent Type Theory
執筆形態	共著
掲載誌名	TPHOLs 2003, Lecture Notes in Computer Science, vol. 758
巻・号・頁	pp.188-203
著者・共著者	Peter Dybjer, Qiao Haiyan, Makoto Takeyama
概要	We extend the proof assistant Agda/Alfa for dependent type theory with a modified version of Claessen and Hughes' tool QuickCheck for random testing of functional programs. In this way we combine testing and proving in one system. Testing is used for debugging programs and specifications before a proof is attempted. Furthermore, we demonstrate by example how testing can be used repeatedly during proof for testing suitable subgoals. Our tool uses testdata generators which are defined inside Agda/Alfa. We can therefore use the type system to prove properties about them, in particular surjectivity stating that all possible test cases can indeed be generated.