米兰体育app下载 关于 VDM 规范的验证和使用 PVS 的细化

引用

Agerholm S、Bicarregui J 和 Maharaj S (1998) 关于 VDM 规范的验证和使用 PVS 的细化。见：Bicarregui J（编辑）VDM 中的证明：案例研究。计算和信息技术的正式方法（FACIT）。伦敦：Springer，第 157-189 页。 http://link.springer.com/chapter/10.1007/978-1-4471-1532-8_6#

摘要
本章介绍如何使用 PVS 系统作为支持 VDMSL 的工具。可以以非常简单和直接的方式将 VDM-SL 翻译为 PVS 规范语言，从而可以使用 PVS 进行类型检查和验证 VDM-SL 规范和改进的属性。翻译有详细的描述并举例说明。翻译的缺点是必须手动完成（尽管自动化可能是可能的），并且所使用的“浅嵌入”技术不能准确捕获 VDM-SL 的证明规则。好处来自于这样的事实：VDM-SL 可以表示的部分是巨大的，并且能够使用强大的 PVS 校对器是一个很大的优势。本章描述了使用 PVS 进行验证的各种示例。