看起来很简单：例如，如果有任何非最终字段访问，处理器会在一个类上使用 @Immutable 。它必须确保所有合作者也是不可变的。
可以将@ReferentiallyTransparent（更好的名称？）放在方法上，然后检查以确保所有调用和协作者也被标记为@RefTrans 和@Immutable ...
问问题
72 次
1 回答
2
您可能对以下论文感兴趣：Java 中的可验证功能纯度
抽象的 ：
证明代码库中的特定方法在功能上是纯的——确定性且无副作用——将有助于验证安全属性，包括函数可逆性、计算的可重复性和不受信任的代码执行的安全性。到目前为止，在广泛使用的高级命令式语言（例如 Java）中，还无法自动证明方法在功能上是纯的。我们讨论了一种技术，通过在称为 Joe-E 的 Java 子集中编写程序来证明方法在功能上是纯的；静态验证器确保程序属于子集。在 Joe-E 中，可以从它们的方法签名中轻松识别纯方法。为了证明我们方法的实用性，我们重构了一个 AES 库，一个实验性的投票机实现，和一个 HTML 解析器来使用我们的技术。我们证明了他们的顶级方法是可验证的纯方法，并展示了这如何为这些例程提供高级安全保证。我们的可验证纯度方法是一种有吸引力的方法，它允许对安全属性进行函数式推理，同时利用命令式语言的熟悉性、便利性和遗留代码。
于 2010-12-20T22:37:39.953 回答