java - Javaで参照透過性、不変性などを強制するプロセッサ/プラグインはありますか?

Question

非常に簡単に思えます。たとえば、クラスの @Immutable は、最終フィールド以外のアクセスがあった場合にプロセッサがエラーを発生させます。すべてのコラボレーターも不変であることを保証する必要があります。

@ReferentiallyTransparent (より良い名前?) をメソッドに配置して、すべての呼び出しと共同作業者にも @RefTrans と @Immutable のマークが付けられていることを確認します...

Answer 1

次の論文に興味があるかもしれません: Verifiable Functional Purity in Java

概要 ：

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