4.10.1.2: Clarify array types in verification type system

The array manipulation instructions {ba,ca,sa}{load,store} are verified using verification types arrayOf({byte,char,short,boolean}), and the newarray instruction can generate typestates featuring the verification types arrayOf({byte,char,short,boolean}). Nevertheless, the verification type system does not include types spelled "byte", "char", "short", or "boolean".

The way out of this mess is to observe that array types, being reference types within the opaque "Java reference type hierarchy", are permitted to have many weird and wonderful things as their element types -- it's of no concern to the rest of the verification type system that functors like class(..), arrayOf(..), and fooBarQuux(..) are deployed for Java reference types. So, while the primitive types byte, char, short, and boolean cannot have unique representation in the verification type system -- they all map to int -- array types with byte, char, short, and boolean as their element types CAN have a unique representation. (In the StackMapTable attribute, the descriptors I, B, C, S, and Z are all encoded with the same verification_type_info tag -- Integer_variable_info -- while [B, [C, [S, and [Z can each be tagged as an Object_variable_info with an appropriate CP reference.)

Here is suggested text for 4.10.1.2:

- Array types correspond to verification types that use the functor arrayOf:
  - The verification type arrayOf(T) represents the array type whose component type is the verification type T.
  - The verification type arrayOf(byte) represents the array type whose element type is byte.
  - The verification type arrayOf(char) represents the array type whose element type is char.
  - The verification type arrayOf(short) represents the array type whose element type is short.
  - The verification type arrayOf(boolean) represents the array type whose element type is boolean.

  Although the primitive types byte, short, char, and boolean do not have unique representations in the verification type system, every array type whose element type is byte, short, char, or boolean DOES have a unique representation in the verification type system. (The {ba,ca,sa}{load,store} and newarray instructions work with array types whose element type is primitive.)

  For example, the types byte[] and boolean[][] would be represented by the verification types arrayOf(byte) and arrayOf(arrayOf(boolean)) respectively.
...
- The other verification types - top, oneWord, twoWord, and reference -- are represented in Prolog as atoms whose name denotes the verification type in question. (The atoms byte, char, short, and boolean which may appear as arguments to arrayOf are NOT verification types.)