研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	2005
形態種別	学術雑誌
査読	査読あり
標題	対話型証明支援ツールPVSの紹介
執筆形態	共著
掲載誌名	コンピュータソフトウェア,Vol.22,No3
巻・号・頁	22(3),37-57頁
著者・共著者	高木理, 渡邊宏, 武山誠
概要	本論文の目的は，証明支援ツールの1 つであるPVSおよびその応用例を紹介することである．第1節および第2節において，PVSおよびその作業の流れを大まかに説明する．第3節および第4節では，PVSにおける最も重要な概念である型および証明に関する説明を行う．第5節において，PVSの応用例として，特定の文字列を分類・変換する簡単なプログラムを取り上げ，PVSを用いてそのプログラムの検証を行う．