Есть ли процессор / плагин, который бы обеспечивал ссылочную прозрачность, иммутабилит и т. Д. В Java?

Question

Это кажется довольно простым: например, @Immutable для класса, в котором процессор мог бы выдавать ошибку, если бы был какой-либо неконечный доступ к полю.Это должно было бы гарантировать, что все соавторы также были неизменяемыми.

@ReferentiallyTransparent (лучше имя?) Можно было бы поместить в методы, которые затем проверяли бы, чтобы все вызовы и соавторы были также помечены @RefTrans и @Immutable...

Answer 1

Вас может заинтересовать следующая статья: Проверяемая функциональная чистота в Java

Аннотация:

Доказательство того, что конкретные методы в базе кода функциональночисто - детерминированный и без побочных эффектов - поможет проверить свойства безопасности, включая обратимость функций, воспроизводимость вычислений и безопасность выполнения ненадежного кода.До сих пор не было возможности автоматически доказать, что метод является функционально чистым в широко используемом императивном языке высокого уровня, таком как Java.Мы обсуждаем технику, чтобы доказать, что методы функционально чисты, написав программы на подмножестве Java под названием Joe-E;статический верификатор гарантирует, что программы попадают в подмножество.В Joe-E чистые методы можно легко узнать по сигнатуре их метода.Чтобы продемонстрировать практичность нашего подхода, мы реорганизовали библиотеку AES, экспериментальную реализацию машины для голосования и анализатор HTML, чтобы использовать наши методы.Мы доказываем, что их методы верхнего уровня проверяемо чисты, и показываем, как это обеспечивает гарантии безопасности высокого уровня для этих процедур.Наш подход к проверяемой чистоте - это привлекательный способ, позволяющий рассуждать о свойствах безопасности в функциональном стиле, используя при этом привычный, удобный и устаревший код императивных языков.