Is there processor/plugin out there that would enforce referential-transparency, immutabiliyt, etc. in Java?

It seems pretty straightforward: For example, an @Immutable on a class that the processor would then give error if there were any non-final field accesses. It would have to ensure that all collaborators were also immutable.

A @ReferentiallyTransparent (better name?) could be put on methods that would then check to ensure that all calls and collaborators were also marked @RefTrans and @Immutable开发者_StackOverflow...

You may be interested by the following paper : Verifiable Functional Purity in Java

Abstract :

Proving that particular methods within a code base are functionally pure — deterministic and side-effect free — would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use, such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature. To demonstrate the practicality of our approach, we refactor an AES library, an experimental voting machine implementation, and an HTML parser to use our techniques. We prove that their top-level methods are verifiably pure and show how this provides high-level security guarantees about these rou- tines. Our approach to verifiable purity is an attractive way to permit functional-style reasoning about security properties while leveraging the familiarity, convenience, and legacy code of imperative languages.