[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification javachar
enrich byte
 , 
       string-less
 with
   sorts 
      javachar;
   functions 
      mkchar : int → javachar;
      mkchar : string → javachar;
       . .int : javachar → int;
   variables 
      jchar, jchar0, jchar1, jchar2 : javachar; 
   induction 
      javachar generated by mkchar;
   axioms 
      equality :  ⊦ mkchar(i) = mkchar(j) ↔ abs(i) % 2 ^ 16 = abs(j) % 2 ^ 16;
      comment: JLS 4.2: whose values are 16-bit unsigned integers 
         representing Unicode characters.;
       
end enrich