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.

Answer 1

Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling:

• Formalize your language's AST into expressions and statements
• Write a semantics for expressions and statements. Your semantics will need:
  • an evaluation relation, relating expression-state pairs $(e,\sigma)$ to an evaluated expressions with updated state $(e', \sigma')$,
  • an execution relation, relating statement-state pairs $(s, \sigma)$ to output states $\sigma$.
• These will be mutually recursive on each other, and can be a big or small-step semantics, depending on your particular need. Big step is simpler, but worse at modeling non-terminating executions.

This basic structure will get you pretty far. To model Java, you probably want to structure your state set hierarchically, around specific objects, but the basic principles are the same. You'll also want to model dynamic dispatch, so it probably makes sense to transform class methods into functions taking an explicit "this" argument.

An axiomatic semantics i.e. Hoare triples, which define a logic of pre- and post-conditions for statements to model imperative programs. I don't know how these relate to OOP, but I'm sure someone has tried in the 50 years they've been around.

You might also be interested in Software Foundations. It's oriented at reasoning about imperative languages in the Coq theorem prover, but it gives an excellent overview of formal semantics.

Answer 2

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.