• 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
            • Semantics
              • Primitive-function-macros
              • Primitive-values
              • Floating-point-placeholders
              • Pointers
              • Floating-point-value-set-parameters
              • Values
              • Primitive-operations
                • Integer-operations
                • Floating-point-operations
                • Boolean-operations
                  • Boolean-xor
                  • Boolean-neq
                  • Boolean-ior
                  • Boolean-eq
                  • Boolean-and
                  • Boolean-not
              • Primitive-conversions
              • Reference-values
        • 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
  • Primitive-operations

Boolean-operations

Java boolean operations [JLS14:4.2.5].

Here we formalize all the strict operations that take boolean operands and return boolean results.

[JLS14:4.2.5] also lists the conditional operators &&, ||, and ? :, but those are non-strict, and therefore must be formalized as part of expression evaluation.

[JLS14:4.2.5] also lists the string concatenation operator +, but that is best formalized in terms of a boolean-to-string conversion, elsewhere.

Subtopics

Boolean-xor
Logical exclusive disjunction ^ [JLS14:4.2.5] [JLS14:15.22.2].
Boolean-neq
Non-equality != on booleans [JLS14:4.2.5] [JLS14:15.21.2].
Boolean-ior
Logical inclusive disjunction | [JLS14:4.2.5] [JLS14:15.22.2].
Boolean-eq
Equality == on booleans [JLS14:4.2.5] [JLS14:15.21.2].
Boolean-and
Logical conjunction & [JLS14:4.2.5] [JLS14:15.22.2].
Boolean-not
Logical complement ! [JLS14:4.2.5] [JLS14:15.15.6].