SimpleJava: Powerful expressions are as expressive as simple ones.
Expressions in Java can have very complex effects in a program state, the combination of short-circuit evaluation and functions with side-effects allow. For example, due to the possibility of side-effects in expressions, one can conceive loops where the conditional statement contains all the code needed for the loop (that is, the loop is correct and yet it has no body). Similarly, due to short circuit evaluation one can write a correct recursive function where the only statement of the body contains a recursive call that would only be made if a progress metric was decreased. As a result of this complexity, generating verification conditions (VCs) directly from Java source code would require a too complex a tool. I propose a translation from Java code to JavaSimple, a simpler language that would allow for a simpler VC generator. JavaSimple is not a new language, it a subset of Java where the complexity of expressions is greatly restricted (for example, the use of both the '&&' and '||' operators is forbidden). I will discuss how to translate any Java source to a JavaSimple source as well as a tool that does this automatically.