[ jmlspecs-Patches-1987810 ] elemtype patch

[SourceForge.net]

Patches item #1987810, was opened at 2008-06-08 10:40
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=510631&aid=1987810&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: None
Group: None
Status: Open
Resolution: None
Priority: 5
Private: No
Submitted By: jlee (jooyong_lee)
Assigned to: Nobody/Anonymous (nobody)
Summary: elemtype patch

Initial Comment:
<Overview>

1. implemented lexing, parsing and type resolution for elemtype
expressions.

2. slightly modified the JmlTypeExpression.resolveType method.

3. The attached update on TypeTest.java contains tests for elemtype.

[java.g]

* added a rule for elemtype expressions as well as keyword
  slash_elemtype.

[Parser.java]

* made token TokenNameslash_elemtypeof consumed in the same way as
  token TokenNameslash_type.

[Scanner.java etc.]

* usual changes

[JmlUnaryExpression.java]

* reorganized resolveType method for better readability.

* added the resolveTypeForTypeof method that basically does the same
  job as done in the previous resolveType method that covered only
  typeof expressions.

* added the resolveTypeForElemtypeof method for elemtype
  expressions. The logic of this method is the same the one of
  resolveTypeForTypeof except for the following:

  1. Field targetType is assigned the type of array elements.  
   
      N.B. In the case of multiarrays, say int[][], the element type
      of it is deemed as int[], not int.

  2. The argument type of an elemtypeof expression is
  java.lang.Class. There are three cases to consider:

   (1) the argument is a type expression, e.g.,
   \elemtypeof(\type(int[])). The targetType field of this.expression
   provides necessary type information.

   (2) the argument is a typeof expression, e.g.,
   \elemtyeof(\typeof(i)). The targetType field of this.expression
   provides necessary type information.

   (3) the argument is a Class-type variable, .e.g., \elemtypeof(c)
   where \typeof(c) is java.lang.Class. Although it looks as if
   appropriate type information could be retrieved from the argument,
   currently, a raw-type class, i.e., java.lang.Class with no type
   parameter, is returned while maintaining the soundness of type
   resolution.

[JmlTypeExpression.java]

* dropped the code that boxes targetType of base types because there
  is a case this boxing causes a strange behavior like predicate
  (Class<Integer> == Class<Integer>) is false.

[OperatroExpression.java]

* Added a case for a elemtype expression in method operatorToString.

[OperatorIds.java]

* Added JML_ELEMTYPEOF.


<Additional Note w.r.t. RAC>

It should be warned not to use the resolvedType fields of
JmlUnaryExpression and JmlTypeExpression when to generate RAC. This is
because

1) Dynamic types may not be determined at type resolution time. The
resolvedType field may not have the most precise type information.

2) The current implementation of JmlTypeExpression and
JmlUnaryExpression does not seem to assign an object-specific class to
the resolvedTypeFields. Currently, the Scope.getJavaLangClass() method
is being used to get the values of Class type to assign to
resolvedType fields; this method does not seem to distinguish classes
seeing as it gets no argument.

3) Except for the cases of dynamic types, it still might be possible
to use resolvedType fields since type variables convey type
information. For example, Class<Integer> means an Integer
type. However, this approach fails over JDTs under 1.5.

Except for the cases of dynamic types, the targetType field can be
used to get type information regardless of JDK versions. For the case
of typeof expressions, it will be necessary to update targetField (or
perhaps add a fresh field) in RAC phase so that it holds the most
precise type information.

In summary, the main purpose of the resolvedType field is for type
checking. If the most precise type information is required, other
fields such as targetField should be used under the assumption that
that field is properly updated at runtime.


Jooyong Lee
Kansas State University



----------------------------------------------------------------------

You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=510631&aid=1987810&group_id=65346

-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers