文章基本信息

标题：対話型証明支援ツールPVSの紹介
本地全文：下载
作者：高木理 ; 渡邊宏 ; 武山誠等
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2005
卷号：22
期号：3
页码：3_37-3_57
DOI：10.11309/jssst.22.3_37
出版社：Japan Society for Software Science and Technology
摘要：
本論文の目的は，証明支援ツールの1 つであるPVSおよびその応用例を紹介することである．第1節および第2節において，PVSおよびその作業の流れを大まかに説明する．第3節および第4節では，PVSにおける最も重要な概念である型および証明に関する説明を行う．第5節において，PVSの応用例として，特定の文字列を分類・変換する簡単なプログラムを取り上げ，PVSを用いてそのプログラムの検証を行う．