|
|
|---|
|
|
|
|---|
Unicode characters in Java [JLS14:3.1].
The Unicode standard distinguishes among `characters', `code points', and `code units'. In Java, characters are essentially Unicode UTF-16 code units, i.e. unsigned 16-bit values. In our formalization, as in [JLS14], we may use the terms `character', `code point', and `code unit' fairly interchangeably, when that causes no confusion.