Axiomatic Semantics for Java^{ℓight} – Extended Abstract –

David von Oheimb^{⋆}

Technische Universität München

                   http://www.in.tum.de/~oheimb/

Abstract. We introduce a Hoare-style calculus for a nearly full subset of sequential Java, which we call Java^{ℓight}. This axiomatic semantics has been proved sound and complete w.r.t. our operational semantics of Java^{ℓight}, described in earlier papers. The proofs also give new insights into the role of type-safety. All the formalization and proofs have been done with the theorem prover Isabelle/HOL.

1 Introduction

Since languages like Java are widely used in safety-critical applications, verification of object-oriented programs has grown more and more important. A first step towards verification seems to be developing a suitable axiomatic semantics (a.k.a. “Hoare logic”) for such languages.

Recently several proposals for Hoare logics for object-oriented languages, e.g. [dB99,PHM99,HJ00], have been given. Typically they deal with some small core language and are partially proved sound on paper (except for [HJ00], which has been machine-checked). None of them has been proved complete. Our new logic, in part inspired by [PHM99], has the following special merits.

– Apart from static overloading and dynamic binding of methods as well as references to dynamically allocated objects, it also covers full exception handling, static fields and methods, and static initialization of classes. Thus our sequential sublanguage Java^{ℓight} is almost the same as Java Card[Sun99].

– Instead of modeling expressions with side-effects as assignments to intermediate variables, it handles all expressions and variables first-class. Thus programs to be verified do not need to undergo an artificial structural transformation.

– It is both sound – w.r.t. a mature formalization of the operational semantics of Java – and complete. This means that programs using even non-trivial features like mutual recursion, dynamic binding, and static initialization can be proved correct.

– Apart from being rigorously and unambiguously defined (in the interactive theorem proving system Isabelle/HOL[Pau94]), it has been proved sound and complete within the system. This gives maximal confidence in the results obtained.

⋆ Research funded by the DFG Project Bali, http://isabelle.in.tum.de/Bali/

2 Some basics of the Java^{ℓight} formalization

Our axiomatic semantics inherits all features concerning type declarations and the program state from our operational semantics of Java^{ℓight}. See [ON99] for a more detailed description.

Here we just recall that a program Γ (which serves as the context for most judgments) consists of a list of class and interface declarations and that the execution state is defined as

datatype st = st (globs) (locals) types state = xcpt option × st

where globs and locals map class references to objects (including class objects) and variable names to values, respectively, and xcpt references an exception object. Using the projection operators on tuples, we define e.g. normal σ ≡ fst σ = None, which expresses that in state σ there is no pending exception, and write snd σ to refer to the state without the information on exceptions, typically denoted by s.

A term of Java^{ℓight} is either an expression, a statement, a variable, or an expression list, and has a corresponding result. For uniformity, even a statement has a (dummy) result, called Unit. The result of a variable is an lval, which is a value (for read access) and a state update function (for write access).

types terms = (expr + stmt) + var + expr list types vals = val + lval + val list types lval = val × (val → state → state)

There are many other auxiliary type and function definitions which we cannot define here for lack of space. The complete Isabelle sources, including an example,

may be obtained from http://isabelle.in.tum.de/Bali/src/Bali4/.

3 The axiomatic semantics

3.1 Assertions

In our axiomatic semantics we shallow-embed assertions in the meta logic HOL, i.e. define them as predicates on (basically) the state, making the dependence on the state explicit and simplifying their handling within Isabelle. This general approach is extended in two ways.

– We let the assertions depend also on so-called auxiliary variables (denoted by the meta variable Z of any type α), which are required to relate variable contents between pre- and postconditions, as discussed in [Sch97].

– We extend the state by a stack (implemented as a list and denoted byY) of result values of type res, which are used to transfer results between Hoare triples. In an operational semantics, these nameless values can be referred to via meta variables, but in an axiomatic semantics, such a simple technique is impossible since all values in a triple are logically bound to that scope (by universal quantification).

As a result, we define the type of assertions (with parameter α) as

types α assn = res list × state → α → bool datatype res = Res (vals) | Xcpt (xcpt option) | Lcls (locals) | DynT (tname)

We write e.g. Val v as an abbreviation for Res (In1 v), injecting a value v into res. Names like Val and DynT are used not only as constructors, but also as (destructor) patterns. For example, λVal v :Y. f v Y is a function on the result stack that expects a value v as the top element and passes it to f together with the rest of the stack, referred to byY.

In order to keep the Hoare rules short and thus more readable, we define several assertion (predicate) transformers.

– λs : P s ≡ λ(Y,σ). P (snd σ) (Y,σ) allows P to peek at the state directly.

– P ∧. p ≡ λ(Y,σ) Z. P (Y,σ) Z ∧ p σ means that not only P holds but also p (applied to the program state only). The assertion Normal P ≡ P ∧. normal is a simple application stating that P holds and no exception has occurred.

– P←:f ≡ λ(Y,σ). P (Y,f σ) means that P holds for the state transformed by f.

– P ;. f ≡ λ(Y,σ′) Z. ∃σ. P (Y,σ) Z ∧ σ′ =f σ means that P holds for some state σ and the current state is then derived from σ by the state transformer f.

3.2 Hoare triples and validity

We define triples as judgments of the form prog⊢{α assn} terms≻ {α assn} with some obvious variants for the different sorts of terms, e.g. Γ ⊢{P} e-≻ {Q} ≡ Γ ⊢{P} In1(Inl e)≻ {Q} and {P} .c. {Q} ≡ {P} In1(Inr c)≻ {Q}.

Here we simplify the presentation by leaving out triples as assumptions within judgments, which are necessary to handle recursion; we have discussed this issue in detail in [Ohe99]. The validity of triples is defined as

Γ ⊧{P} t≻ {Q} ≡ ∀Y σ Z. P (Y,σ) Z ⟶ type ok Γ t σ ⟶ ∀v σ′. Γ ⊢σ −t≻→ (v,σ′) ⟶ Q (res t v Y,σ′) Z

where Y stands for the result stack and Z denotes the auxiliary variables. The judgment type ok Γ t σ means that the term t is well-typed (if σ is a normal state) and that all values in σ conform to their static types. This additional precondition is required to ensure soundness, as discussed in §3.5. Γ ⊢σ −t≻→ (v,σ′) is the evaluation judgment from the operational semantics meaning that from the initial state σ the term t evaluates to a value v and final state σ′. Note that we define partial correctness.

Unless t is statement, the result value v is pushed onto the result stack via res t v Y ≡ if is stmt t then Y else Res v :Y.

3.3 Result value passing

We define the following abbreviations for producing and consuming results:

– P↑:w ≡ λ(Y,σ). P (w :Y,σ) means that P holds where the result w is pushed.

– λw :. P w ≡ λ(w :Y,σ). P w (Y,σ) expects and pops a result w and asserts P w. A typical application of the former is the rule for literal values v:

Lit

Γ ⊢{Normal (P↑:Val v)} Lit v-≻ {P}

Analogously to the well-known assignment rule, it states that for a literal expression (i.e., constant) v the postcondition P can be derived if P – with the value v inserted – holds as the precondition and the (pre-)state is normal.

The rule for array variables handles result values in a more advanced way:

AVar \frac{Γ ⊢\{Normal P\} e_{1}-≻ \{Q\} Γ ⊢\{Q\} e_{2}-≻ \{λVal i :. RefVar (avar Γ i)\}}{Γ ⊢\{Normal P\} e_{1}[e_{2}]=≻ \{R\}}

where RefVar vf P ≡ λ(Val a :Y,(x,s)). let (v,x′) = vf a x s in (P↑:Var v) (Y,(x′,s)). Both subexpressions are evaluated in sequence, where Q as intermediate assertion typically involves the result of e_{1}. The final postcondition R is modified for the proof on e_{2} as follows: from the result stack two values are expected and popped, namely i (the index) and a (an address) of e_{2} and e_{1}, respectively. Out of these and the intermediate state (x,s), the auxiliary function avar computes the variable v, which is pushed as the final result, and (possibly) an exception x′.

For terms involving a condition, we define the assertion P↑:Bool=b ≡ λ(Y,σ) Z. ∃v. (P↑:Val v) (Y,σ) Z ∧ (normal σ ⟶ the Bool v = b) expressing (basically) that the result of a preceding boolean expression is b. Together with the meta-level conditional expression (if b then e_{1} else e_{2}) depending on b and P′↑:Bool=b identifying b with the result of a boolean expression e_{0}, we can describe both branches of conditional terms with a single triple, like in

Cond \frac{Γ ⊢\{Normal P\} e_{0}-≻ \{P′\} ∀b. Γ ⊢\{P′↑:Bool=b\} (if b then e_{1} else e_{2})-≻ \{Q\}}{Γ ⊢\{Normal P\} e_{0} ? e_{1} : e_{2}-≻ \{Q\}}

The value b is universally quantified, such that when applying this rule, one has to prove its second antecedent for any possible value, i.e., both True and False. What is a notational convenience here (to avoid two triples, one for each case), will be essential for the Call rule, given below.

The rules for the standard statements appear almost as usual:

Skip \overline{Γ ⊢\{P\} .Skip. \{P\}}  Loop \frac{Γ ⊢\{P\} e-≻ \{P′\} Γ ⊢\{P′↑:Bool=True\} .c. \{P\}}{Γ ⊢\{P\} .while(e) c. \{P′↑:Bool=False\}}

Note that in all^{1} rules (except Loop for obvious reasons) the postconditions of the conclusion is a variable. Thus in the typical “backward-proof” style of Hoare logic the rules are applied easily.

3.4 Dynamic binding

The great challenge of an axiomatic semantics for an object-oriented language is dynamic binding in method calls, for two reasons.

First, the code selected depends on the class D dynamically computed from a reference expression e. The range of values for D depends on the whole program and thus cannot be fixed locally, in contrast to the two possible boolean values appearing in conditional terms described above. Standard Hoare triples cannot express such an unbound case distinction. We handle this problem with the strong technique given above, using universal quantification and the precondition R↑:DynT D ∧… with the special result value DynT D. An alternative solution is

1 The rules not mentioned here may be found in the appendix.

given in [PHM99], where D is referred to via This and the possible variety of D is handled in a cascadic way using several special rules.

Second, the actual value D often can be inferred statically, but in general for invocation mode “virtual”, one can only know that it is a subtype of some reference type rt computed by static analysis during type-checking. The intuitive – but absolutely non-trivial – reason why the subtype relation Class D⪯RefT rt holds is of course type-safety. The problem here is how to establish this relation. The rules given in [PHM99], for example, put the burden of verifying the relation on the user, which is possible, but in general not practically feasable. In contrast, our solution make the relation available to the user as a helpful assumption (see the subformula Γ ⊢mode→D⪯rt in the rule given below), which transfers the proof burden once and for all to the soundness proof on the meta-level.

The remaining parts of the rule for method calls deals with the unproblematic issues of argument evaluation, setting up the local variables (including parameters) of the called method and restoring the previous local variables on return, for which we use the special result value Lcls.

Call

Γ ⊢{Normal P} e-≻ {Q}

Γ ⊢{Q} args≐≻ {λVals vs :Val a :. λs : let D = dyn class mode s a τ in R↑:DynT D↑:Lcls (locals s)←:init lvars Γ D (mn,pTs) mode a vs}

∀D. Γ ⊢{R↑:DynT D ∧.λσ. normal σ ⟶ Γ ⊢mode→D⪯rt}

Body D (mn,pTs)-≻ {λVal v :Lcls l :. S↑:Val v←:set lvars l} Γ ⊢{Normal P} {rt,τ,mode}e.mn({pTs}args)-≻ {S}

3.5 Soundness and completeness

With the help of Isabelle/HOL, we have proved soundness and completeness:

wf prog Γ ⟹ Γ ⊧{P} t≻ {Q} = Γ ⊢{P} t≻ {Q}

where wf prog Γ means that the program Γ is well-formed. As usual, soundness is proved by rule induction on the derivation of triples. Surprisingly, type-safety plays a crucial role here. The important fact that for method calls the subtype relation Class D⪯RefT rt holds can be derived only if the state conforms to the environment. This was the reason for bringing the judgment type ok into our definition of validity, which also gives rise to the new rule (required for the completeness proof)

hazard

Γ ⊢{P ∧. Not ∘ type ok Γ t} t≻ {Q}

indicating that if at any time conformance was violated, anything could happen.

Completeness is proved (basically) by structural induction with the MGF approach discussed in [Ohe99]. This includes an outer auxiliary induction on the number of methods already verified, which requires well-typedness in order to ensure that for any program there is only a finite number of methods to consider. Due to class initialization, an extra induction on the number of classes already initialized is required.

References

[dB99] Frank de Boer. A WP-calculus for OO. In Foundations of Software Science and Computation Structures, volume 1578 of LNCS. Springer-Verlag, 1999.

[HJ00] Marieke Huisman and Bart Jacobs. Java program verfication via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering (FASE’00), LNCS. Springer-Verlag, 2000. to appear.

[Ohe99] David von Oheimb. Hoare logic for mutual recursion and local variables. In C. Pandu Rangan, V. Raman, and R. Ramanujam, editors, FST&TCS’99, volume 1738 of LNCS, pages 168–180. Springer-Verlag, 1999.

[ON99] David von Oheimb and Tobias Nipkow. Machine-checking the Java specification: Proving type-safety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of LNCS. Springer-Verlag, 1999.

http://isabelle.in.tum.de/Bali/papers/Springer98.html.

[Pau94] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994. For an up-to-date description, see

http://isabelle.in.tum.de/.

[PHM99] Arnd Poetzsch-Heffter and Peter Müller. A programming logic for sequential Java. In S. D. Swierstra, editor, Programming Languages and Systems (ESOP ’99), volume 1576 of LNCS, pages 162–176. Springer-Verlag, 1999.

[Sch97] Thomas Schreiber. Auxiliary variables and recursive procedures. In TAP-SOFT’97, volume 1214 of LNCS, pages 697–711. Springer-Verlag, 1997.

[Sun99] Sun. Java Card Spec., 1999. http://java.sun.com/products/javacard/.

A The remaining rules

conseq \frac{∀Y σ Z . P (Y ,σ) Z ⟶ (∃P′ Q′. Γ ⊢\{P′\} t≻ \{Q′\} ∧ (∀w σ′. (∀Y′ Z′. P′ (Y′,σ) Z′ ⟶ Q′ (res t w Y′,σ′) Z′) ⟶ Q (res t w Y ,σ′) Z))}{Γ ⊢\{P\} t≻ \{Q\}}

Xcpt

Γ ⊢{(λ(Y,σ). P (res t (arbitrary3 t) Y,σ)) ∧. Not ∘ normal} t≻ {P}

Super

Γ ⊢{Normal (λs : P↑:Val (val this s))} super-≻ {P}

LVar

Γ ⊢{Normal (λs : P↑:Var (lvar vn s))} LVar vn=≻ {P}

FVar \frac{Γ ⊢\{Normal P\} .init C. \{Q\} Γ ⊢\{Q\} e-≻ \{RefVar (fvar C stat fn) R\}}{Γ ⊢\{Normal P\} \{C,stat\}e.fn=≻ \{R\}}

Acc \frac{Γ ⊢\{Normal P\} va=≻ \{λVar (v,f) :. Q↑:Val v\}}{Γ ⊢\{Normal P\} Acc va-≻ \{Q\}}

Ass \frac{Γ ⊢\{Normal P\} va=≻ \{Q\} Γ ⊢\{Q\} e-≻ \{λVal v :Var (w,f) :. R↑:Val v←:assign f v\}}{Γ ⊢\{Normal P\} va:=e-≻ \{R\}}

Nil

{Normal P↑:Vals []} []≐≻ {P}

Cons \frac{Γ ⊢\{Normal P\} e-≻ \{Q\} Γ ⊢\{Q\} es≐≻ \{λVals vs :Val v :. R↑:Vals (v :vs)\}}{Γ ⊢\{Normal P\} e :es≐≻ \{R\}}

NewC \frac{Γ ⊢\{Normal P\} .init C. \{Alloc Γ (CInst C) id Q\}}{Γ ⊢\{Normal P\} new C-≻ \{Q\}}

where Alloc Γ otag f P ≡

λ(Y,(x,s)) Z. ∀σ′ a. Γ ⊢(f x,s) −halloc otag≻a→ σ′⟶ (P↑:Val (Addr a)) (Y,σ′) Z

NewA \frac{Γ ⊢\{Normal P\} .init comp ty T. \{Q\} Γ ⊢\{Q\} e-≻ \{λVal i :. Alloc Γ (Arr T (the Intg i)) (check neg i) R\}}{Γ ⊢\{Normal P\} new T[e]-≻ \{R\}}

Cast \frac{Γ ⊢\{Normal P\} e-≻ \{λVal v :. Q↑:Val v←:λ(x,s). (raise if (¬Γ,s⊢v fits T) ClassCast x,s)\}}{Γ ⊢\{Normal P\} Cast T e-≻ \{Q\}}

Inst \frac{Γ ⊢\{Normal P\} e-≻ \{λVal v :. λs : (Q↑:Val (Bool (v≠Null ∧ Γ,s⊢v fits RefT T)))\}}{Γ ⊢\{Normal P\} e instanceof T-≻ \{Q\}}

Body \frac{the (cmethd Γ C sig) = (md, , , blk, res) Γ ⊢\{Normal P\} .init md. \{Q\} Γ ⊢\{Q\} .blk. \{R\} Γ ⊢\{R\} res-≻ \{S\}}{Γ ⊢\{Normal P\} Body C sig-≻ \{S\}}

Expr \frac{Γ ⊢\{Normal P\} e-≻ \{λw :. Q\}}{Γ ⊢\{Normal P\} .Expr e. \{Q\}} Comp \frac{Γ ⊢\{Normal P\} .c_{1}. \{Q\} Γ ⊢\{Q\} .c_{2}. \{R\}}{Γ ⊢\{Normal P\} .c_{1};c_{2}. \{R\}}

If \frac{Γ ⊢\{Normal P\} e-≻ \{P′\} ∀b. Γ ⊢\{P′↑:Bool=b\} .(if b then c_{1} else c_{2}). \{Q\}}{Γ ⊢\{Normal P\} .if(e) c_{1} else c_{2}. \{Q\}}

Throw \frac{Γ ⊢\{Normal P\} e-≻ \{λVal a :. Q←:λ(x,s). (throw a x,s)\}}{Γ ⊢\{Normal P\} .throw e. \{Q\}}

Try \frac{Γ ⊢\{Normal P\} .c_{1}. \{Q\} Γ ⊢\{(Q ∧.λσ. Γ,σ⊢catch C) ;. new xcpt var vn\} .c_{2}. \{R\} Γ ⊢\{Q ∧.λσ. ¬Γ,σ⊢catch C\} .Skip. \{R\}}{Γ ⊢\{Normal P\} .try c_{1} catch(C vn) c_{2}. \{R\}}

Fin \frac{Γ ⊢\{Normal P\}.c_{1}.\{λ(Y,(x,s)). (Q↑:Xcpt x) (Y,(None,s))\} Γ ⊢\{Normal Q\}.c_{2}.\{λXcpt x′:. R←:λ(x,s). (xcpt if (x′≠None) x′ x,s)\}}{Γ ⊢\{Normal P\} .c_{1} finally c_{2}. \{R\}}

Done

Init

Γ ⊢{Normal (P ∧. initd C)} .init C. {P} the (class Γ C) = (sc, , , ,ini) sup = if C = Object then Skip else init sc Γ ⊢{Normal ((P ∧. Not ∘ initd C) ;. supd (new stat obj Γ C))} .sup. {Q↑:.λs. Lcls (locals s)}

Γ ⊢{Q ;. set lvars empty} .ini. {λLcls l :. R←:set lvars l}

Γ ⊢{Normal (P ∧. Not ∘ initd C)} .init C. {R}