Reasoning about Java Classes (Preliminary Report)
Reasoning about Java Classes (Preliminary Report)
复制标题
关于 Java 类的推理（初步报告）
DOI：
10.1145/286942.286973
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
M. Berkum
中科院分区：
文献类型：
--
作者：
B. Jacobs;J. Berg;M. Huisman;M. Berkum
我们展示了一个名为 LOOP 的项目的第一个成果，该项目涉及面向对象语言 Java 的形式化方法。它的目的是在现代工具的支持下验证程序属性。我们使用我们自己的前端工具（部分仍在构建中）将 Java 类转换为高阶逻辑，并使用后端定理证明器（即 PVS，在 SRI 开发）进行推理。在几个示例中，我们演示了如何按照这种两步方法来证明 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.