7
$\begingroup$

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.

$\endgroup$
3
  • 3
    $\begingroup$ Maybe the papers about "Featherweight Java" are relevant. It's been a while since I read something about that, but they tried to define a reasonably small Java subset which is still general enough and admits a decently-sized semantics. Doing this for full Java is overkill: the official language specification is 700ish pages of informal descriptions, IIRC. $\endgroup$
    – chi
    Oct 13, 2017 at 17:28
  • $\begingroup$ Yeah, I took one look at the specs and kept going. Also, that's only the language specs IIR - the JVM specs have another 600-700 pages. I'll look into Featherweight Java, though. Thanks for the suggestion $\endgroup$ Oct 13, 2017 at 17:30
  • $\begingroup$ Oh wow, Pierce and Wadler! I'll be reading this regardless of its applicability to my work :D $\endgroup$ Oct 13, 2017 at 17:32

2 Answers 2

7
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ The original Hoare triples/axiomatic semantics didn't handle higher-order constructs such as first-class function and objects. More modern approaches such as the logic of bunched implications particularly in the form of separation logic, and Hoare type theory do provide an approach that can handle such features. $\endgroup$ Oct 14, 2017 at 8:33
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.