论文标题
验证,分析和转换工具的序言
Prolog for Verification, Analysis and Transformation Tools
论文作者
论文摘要
本文研究了序言语言在编写验证,分析和转换工具中的使用。在教学经验和开发验证工具(例如概率或专业化工具)等验证工具(例如ECCE和Logen)的指导下,本文介绍了对Prolog的各个方面的评估,并提供了使用它们的指南。文章显示了一些关键序言特征的有用性。特别是,它讨论了如何在要验证或分析的对象程序级别上处理否定。
This article examines the use of the Prolog language for writing verification, analysis and transformation tools. Guided by experience in teaching and the development of verification tools like ProB or specialisation tools like ECCE and LOGEN, the article presents an assessment of various aspects of Prolog and provides guidelines for using them. The article shows the usefulness of a few key Prolog features. In particular, it discusses how to deal with negation at the level of the object programs being verified or analysed.