Без заголовка

У меня есть концепция lightweight тулзы для верификации рефакторинга. Грубо говоря, задача работать с методами без рекурсии и без циклов (либо примитивные циклы). Эта задача при вышеуказанных ограничениях достаточно легко решается - строишь contorl flow graph, поскольку циклов нет (примитивные циклы можно разворачивать), то он представляет собой дерево. По каждому пути в дереве строишь символические уравнения, они достаточно просто решаются солверами (если циклов нет или они простые). Есть конечно технические сложности с парсингом Джавы (хотя можно работать на уровне байткода) плюс с семантикой языка, но тулзу сделать в целом несложно. Самое главное это конечно знать как и где ее применять :). Но я знаю класс задач, для которых она была бы полезна в реальных проектах: рефакторинг лапшеобразного кода внутри циклов. Я с такими проблемами часто сталкивался.