Reasoning about Java classes: preliminary report
Reasoning about Java classes: preliminary report
复制标题
关于 Java 类的推理：初步报告
DOI：
10.1145/286936.286973
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
H. Tews
中科院分区：
文献类型：
--
作者：
B. Jacobs;J. Berg;M. Huisman;M. Berkum;U. Hensel;H. Tews
我们介绍了一个名为LOOP的项目的第一个结果，该项目是针对对象语言Java的形式方法。它旨在在现代工具的支持下验证程序属性。我们使用自己的前端工具（仍在部分建设中）将Java类转换为高阶逻辑，以及用于推理的后端定理Prover（即SRI开发的PVS）。在几个示例中，我们证明了如何在这种两步的方法之后证明Java程序和类的非平凡属性。
We present the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our own front-end tool (which is still partly under construction) for translating Java classes into higher order logic, and a back-end theorem prover (namely PVS, developed at SRI) for reasoning. In several examples we demonstrate how non-trivial properties of Java programs and classes can be proven following this two-step approach.