Formal model of execution for Java (or general imperative language)

Question

I'm trying to prove some statements about execution in Java programs under some heavy restrictions (basically I have a conjecture that if two methods satisfy a set of constraints for a given input then the are they equivalent - i.e., that return value and state after execution are identical). To prove this I'm looking for some sort of formalism that will let me talk about this.

I'm familiar with the operational semantics of functional languages and I could possibly translate for loops/while loops to recursive functions... I'd rather not do this and it would be nice to have some machinery so I could stay in imperative land.

More specifically, I want to reason about the state of a method at the kth step of execution. This includes global state:

• Calls like this.field = 2 update our class state
• Calls modifying parameters update state outside of our method:
  • myParam.setFoo(...)
  • myParam.x = y
• Calls to static methods
  • Blah.static_side_effects()

I am assuming that all of this is deterministic. That is, I want to formalize the assumption that if any of these global updates to state occur in two methods, both of whose global and local execution states are identical, then the new state will also be identical - that each step of computation is determined precisely by global state and local state. This obviously precludes RNGs and parallelism (but I may deal with this later...).

Any ideas or sources on how I could approach this? My only thought is to treat methods as a list of statements and try to describe a statements semantics formally.

If possible I'd love to do this at the Java language level rather than the JVM level. This may not be feasible but my goal for now is to make some reasonable assumptions about my operational semantics and then take it from there.

Oh, one final note - any suggestions on how I can improve this question would be greatly appreciated. I'm kind of flailing around trying to find the right language to ask the question and if I'm abusing terminology (like local/global execution state...) I'd love to correct this.