• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
        • Atj
        • Aij
        • Language
          • Syntax
            • Grammar
            • Unicode-escapes
            • Unicode-input-char
            • Escape-sequence
            • Identifiers
            • Primitive-types
            • Reference-types
            • Keywords
            • Unicode-characters
            • Integer-literals
            • String-literals
            • Octal-digits
            • Hexadecimal-digits
            • Decimal-digits
            • Binary-digits
            • Character-literals
            • Null-literal
            • Floating-point-literals
            • Boolean-literals
            • Package-names
            • Literals
          • Semantics
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Language

Syntax

A formal model of some aspects of the syntax of Java.

It is expected that more aspects of the syntax of Java will be formalized here over time.

Subtopics

Grammar

Grammar of the Java language [JLS14].

Unicode-escapes

First Java lexical translation step: Unicode escapes [JLS14:3.3].

Unicode-input-char

Fixtype of Unicode input characters [JLS14:3.3].

Escape-sequence

Fixtype of escape sequences [JLS14:3.10.6].

Identifiers

Java identifiers [JLS14:3.8].

Primitive-types

Java primitive types [JLS14:4.2].

Reference-types

Java reference types [JLS14:4.3].

Keywords

The Java keywords [JLS14:3.9].

Unicode-characters

Unicode characters in Java [JLS14:3.1].

Integer-literals

Java integer literals [JLS14:3.10.1].

String-literals

Java string literals [JLS14:3.10.5].

Octal-digits

Java octal digits [JLS14:3.10.1].

Hexadecimal-digits

Java hexadecimal digits [JLS14:3.10.1].

Decimal-digits

Java decimal digits [JLS14:3.10.1].

Binary-digits

Java binary digits [JLS14:3.10.1].

Character-literals

Java character literals [JLS14:3.10.4].

Null-literal

Java null literal [JLS14:3.10.7].

Floating-point-literals

Java floating-point literals [JLS14:3.10.2].

Boolean-literals

Java boolean literals [JLS14:3.10.3].

Package-names

Java package names [JLS14:6.5].

Literals

Java literals [JLS14:3.10].