Formal model of execution for Java (or general imperative language)
There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype implementation, it seems that the functionality is being incorporated into the $\mathbb{K}$ framework tools themselves as kprover. Unfortunately, it seems the framework is in the middle of being updated, and getting the framework to build and work appropriately is a bit of a chore, and I'm not really sure how practical and/or functional kprover currently is. You could, however, manually prove things referencing the operational semantics (and also using the Matching Logic proof system if you like). The paper describing the Java semantics, K-Java: A Complete Semantics of Java, references some other systems that are less complete, but may be complete enough for your purposes. That said, they may well not be geared toward proving properties about Java programs. Indeed, in the paper, the semantics is being used for model checking rather than correctness proofs.

This is an answer if you want a high degree of confidence that the actual Java code behaves as you intend. If the goal is more verifying the algorithm than the specific realization into Java, then this is likely overkill. That said, you could easily formalize a simple imperative language in $\mathbb{K}$ if you only need basic imperative/OO features. Indeed, this is done as an exercise in the $\mathbb{K}$ framework tutorial. In fact, if you can reformulate your problem into the fragment of C the Matching Logic prototype supports, you could possibly use that as-is.