Javaに参照透過性、無制限性などを施すプロセッサ/プラグインはありますか？

Question

かなり簡単です： たとえば、最終的なフィールドへのアクセスがなかった場合、プロセッサがエラーを返すクラスに@Mutableがあります。すべての共同作業者も不変であることを保証する必要があります。

A @ReferentiallyTransparent（より良い名前は？）そして、すべての呼び出しとの共同研究も@RefTransと@Immutableをマークしたことを確認するためにチェックする方法に置くことができ...

Answer 1

あなたは以下のことで興味がある可能性があり紙：Verifiable Functional Purity in Java

要約：コードベース内のその特定のメソッドを証明

が機能 純粋である - フリー決定論と副作用 -の検証を助けるであろう関数の可逆性、再現性を含むセキュリティー特性 計算、および信頼できないコード実行の安全性。これまでは、 は、 Javaのように、広く使用されている高水準の命令型言語の中で機能的に機能することを自動的に証明することはできませんでした。 Joe-Eと呼ばれるJavaのサブセットにプログラムを書くことで、メソッドが機能的には純粋であることを証明する手法について説明します。静的な ベリファイアでは、プログラムがサブセットに含まれることが保証されます。 Joe-Eでは、純粋な メソッドは、メソッドのシグネチャから簡単に認識できます。 には、私たちのアプローチの実用性を実証するために、AES ライブラリ、実験的投票機実装、およびHTML パーサーが、この手法を使用するためにリファクタリングされています。彼らの最上位のメソッド は、検証可能に純粋であり、これがどのようにこれらのルーチンについて高レベルのセキュリティ の保証を提供しているかを示しています。検証可能な純度 への私たちのアプローチは、親しみやすさ、便利さ、および命令的言語の従来のコード を活用しながら、 セキュリティプロパティに関する機能スタイルの推論を可能にする魅力的な方法です。