esc/java2 problems with axioms

From: David Cok cok@frontiernet.net Date: 4 March, 2006 20:20:33 GMT To: Michal Moskal michal.moskal@gmail.com, Joe Kiniry <kiniry@acm.org

Subject: Re: esc/java2 problems with axioms Reply-To: cok@frontiernet.net

Joe,

Since you and your students are writing other logics, I thought I would involve you in this discussion.

I agree with Michal that an inconsistency is present here. The right way to resolve it depends on the interpretation of types and of 'is' :-)

The original axioms for numeric types have T_byte, T_int etc. being final types, that is no subtypes. However, numberic values can be more than one type (using is) - is(0,T_byte) and is(0,T_int) are both true.

The typeof function was also originally defined for objects as the dynamic type of a (reference) value. So 'is' works nicely with 'typeof' for reference objects (with the minor complication of null values): (BG_PUSH (FORALL (x t) (PATS (MPAT (<: t |T_java.lang.Object|) (is x t))) (IMPLIES (<: t |T_java.lang.Object|) (IFF (is x t) (OR (EQ x null) (<: (typeof x) t))))))

Note also that is(x,t) is true for many t if x is null, just as when x is a primitive numeric value.

Note that JML allows \typeof to be applied to primitive variables, expressions and literals. It is translated by jmlc as the type of the expression. A literal such as '0' is int. This works because Java distinguishes int literals from long literals etc. Thus in JML, for example, \typeof(0) != \type(byte). \typeof on a primitive expression is translated directly to a literal type value (no use of Simplify's typeof). The logic underlying Simplify just has numeric values. Thus \typeof in JML is somewhat different than typeof in Simplify.

Given all of this, I believe that I was in error to introduce the axioms

'is' on numbers has a kind of subset relationship but not a subtype relationship (since the primitive types are final). At most we can say (IF (EQ (typeof x) |T_byte|) (is x |T_byte|)) But since Simplify's numbers are simply mathematical integers or reals, so defining typeof on Simplify's values is problematic; thus it is probably better not to introduce this axiom schema either.

Unfortunately, I do not have a record of the kind of code for which these axioms were needed to complete a verification.

Thoughts?

David

Michal Moskal wrote:

Hi,

I'm developing a theorem prover and using formulas generated by ESC/Java2 as test cases. I found you have added the following axioms to the set of universal axioms:

The other axioms, previously present there are:

I'm not sure if I got something wrong here, but it seems this prevents my prover from proving toArray() assertions in a few classes. I'm not sure how Simplify handles that, but it doesn't seem right for the axiom set to be inconsitant.

I'm writing just to let you know, I'm not actually using ESC/Java2, just using it as a testcase.

kiniry / Mobius

esc/java2 problems with axioms #85