• 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
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
                • Jbinop
                • Jmethod
                • Jtype
                • Jfield
                  • Jfield-fix
                  • Make-jfield
                  • Jfieldp
                  • Jfield-equiv
                  • Change-jfield
                  • Jfield->volatile?
                  • Jfield->transient?
                  • Jfield->static?
                  • Jfield->init?
                  • Jfield->final?
                  • Jfield->access
                  • Jfield->type
                  • Jfield->name
                • Jexprs
                • Jliteral
                • Junop
                • Jlocvar
                • Jcunit
                • Jaccess
                • Maybe-jexpr
                • Jparam
                • Jimport
                • Jcinitializer
                • Jresult
                • Jstatems+jblocks
                • Jexpr-get-field
                • Jliteral-long-dec-nouscores
                • Nat-to-dec-chars-theorems
                • Jmethods-to-jcbody-elements
                • Jclasses-to-jcbody-elements
                • Jblock-locvar-final
                • Jblock-locvar
                • Jliteral-int-dec-nouscores
                • Jfields-to-jcbody-elements
                • Jblock-for
                • Jblock-smethod
                • Jblock-imethod
                • Jblock-ifelse
                • Jblock-asg-name
                • Jparam-list->types
                • Jparam-list->names
                • Jexpr-lit-long-dec-nouscores
                • Jexpr-lit-int-dec-nouscores
                • Jexpr-literal-string
                • Jexpr-literal-floating
                • Jexpr-literal-character
                • Jblock-while
                • Jblock-method
                • Jblock-if
                • Jblock-expr
                • Jblock-do
                • Jblock-asg
                • Jexpr-name-list
                • Jblock-throw
                • Jblock-return
                • Jparam-list
                • Jimport-list
                • Jexpr-literal-true
                • Jexpr-literal-null
                • Jexpr-literal-false
                • Jexpr-literal-1
                • Jexpr-literal-0
                • Jclass-list
                • Jblock-continue
                • Jtype-short
                • Jtype-long
                • Jtype-list
                • Jtype-int
                • Jtype-float
                • Jtype-double
                • Jtype-char
                • Jtype-byte
                • Jtype-boolean
                • Jmethod-list
                • Jliteral-list
                • Jfield-list
                • Jblock-list
                • Jblock-break
                • Jclasses+jcmembers
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • 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
  • Atj-java-abstract-syntax

Jfield

Java field declarations [JLS14:8.3].

This is a product type introduced by fty::defprod.

Fields
access — jaccess
static? — booleanp
final? — booleanp
transient? — booleanp
volatile? — booleanp
type — jtype
name — stringp
init? — maybe-jexpr

We only capture declarations of single fields, with or without an initializer, and without array square brackets after the name (i.e. all the array square brackets are in the type).

Subtopics

Jfield-fix
Fixing function for jfield structures.
Make-jfield
Basic constructor macro for jfield structures.
Jfieldp
Recognizer for jfield structures.
Jfield-equiv
Basic equivalence relation for jfield structures.
Change-jfield
Modifying constructor for jfield structures.
Jfield->volatile?
Get the volatile? field from a jfield.
Jfield->transient?
Get the transient? field from a jfield.
Jfield->static?
Get the static? field from a jfield.
Jfield->init?
Get the init? field from a jfield.
Jfield->final?
Get the final? field from a jfield.
Jfield->access
Get the access field from a jfield.
Jfield->type
Get the type field from a jfield.
Jfield->name
Get the name field from a jfield.