• 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
                  • Long-long-ushiftr
                  • Long-int-ushiftr
                  • Int-long-ushiftr
                  • Int-int-ushiftr
                  • Long-long-shiftr
                  • Long-long-shiftl
                  • Long-int-shiftr
                  • Long-int-shiftl
                  • Int-long-shiftr
                  • Int-int-shiftr
                  • Int-long-shiftl
                  • Int-int-shiftl
                  • Long-xor
                  • Long-neq
                  • Long-lesseq
                  • Long-ior
                  • Long-greateq
                  • Long-and
                  • Int-xor
                  • Int-ior
                  • Int-greateq
                  • Long-rem
                  • Long-mul
                  • Long-less
                  • Long-great
                  • Long-eq
                  • Long-div
                  • Long-add
                  • Int-neq
                  • Int-mul
                  • Int-lesseq
                  • Int-great
                  • Int-eq
                  • Int-and
                  • Int-add
                  • Long-sub
                  • Int-sub
                  • Int-rem
                  • Int-less
                  • Int-div
                  • Long-plus
                  • Long-not
                  • Long-minus
                  • Int-not
                  • Int-minus
                  • Int-plus
                • Floating-point-operations
                • Boolean-operations
              • 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

Integer-operations

Java integer operations [JLS14:4.2.2].

Here we formalize all the unary and binary operations on integral values that are not conversions (those are formalized separately). The term `integer operations', as opposed to `integral operations', is used in the title of [JLS14:4.2.2].

Since integral values are subjected to unary and binary numeric promotion [JLS14:5.6] [JLS14:15], the operations on integral values actually only operate on int and long values as operands.

For the shift operations [JLS14:15.19], unary numeric promotion is applied to the operands separately. Thus, for each such operation, there are four variants, corresponding to each operand being int or long.

Some integer operations have boolean results.

[JLS14:4.2.2] also lists the prefix and posfix ++ and -- operators, but those operate on variables, not just values, and therefore must be formalized elsewhere.

[JLS14:4.2.2] also lists the conditional operator ? :, but that one is non-strict, and therefore must be formalized as part of expression evaluation.

[JLS14:4.2.2] also lists the string concatenation operator +, but that is best formalized in terms of integral-to-string conversions, elsewhere.

[JLS14:4.2.2] also lists the cast operator, which involves conversions, which, as mentioned above, are formalized separately.

Subtopics

Long-long-ushiftr
Unsigned right shift of an long by an long [JLS14:4.2.2] [JLS14:15.19].
Long-int-ushiftr
Unsigned right shift of a long by an int [JLS14:4.2.2] [JLS14:15.19].
Int-long-ushiftr
Unsigned right shift of an int by a long [JLS14:4.2.2] [JLS14:15.19].
Int-int-ushiftr
Unsigned right shift of an int by an int [JLS14:4.2.2] [JLS14:15.19].
Long-long-shiftr
(Signed) right shift of a long by a long [JLS14:4.2.2] [JLS14:15.19].
Long-long-shiftl
Left shift of a long by a long [JLS14:4.2.2] [JLS14:15.19].
Long-int-shiftr
(Signed) right shift of a long by an int [JLS14:4.2.2] [JLS14:15.19].
Long-int-shiftl
Left shift of a long by an int [JLS14:4.2.2] [JLS14:15.19].
Int-long-shiftr
(Signed) right shift of an int by a long [JLS14:4.2.2] [JLS14:15.19].
Int-int-shiftr
(Signed) right shift of an int by an int [JLS14:4.2.2] [JLS14:15.19].
Int-long-shiftl
Left shift of an int by a long [JLS14:4.2.2] [JLS14:15.19].
Int-int-shiftl
Left shift of an int by an int [JLS14:4.2.2] [JLS14:15.19].
Long-xor
Bitwise exclusive disjunction ^ on longs [JLS14:4.2.2] [JLS14:15.22.1].
Long-neq
Non-equality != on longs [JLS14:4.2.2] [JLS14:15.21.1].
Long-lesseq
Less-than-or-equal-to comparison <= on longs [JLS14:4.2.2] [JLS14:15.20.1].
Long-ior
Bitwise inclusive disjunction | on longs [JLS14:4.2.2] [JLS14:15.22.1].
Long-greateq
Greater-than-or-equal-to comparison >= on longs [JLS14:4.2.2] [JLS14:15.20.1].
Long-and
Bitwise conjunction & on longs [JLS14:4.2.2] [JLS14:15.22.1].
Int-xor
Bitwise exclusive disjunction ^ on ints [JLS14:4.2.2] [JLS14:15.22.1].
Int-ior
Bitwise inclusive disjunction | on ints [JLS14:4.2.2] [JLS14:15.22.1].
Int-greateq
Greater-than-or-equal-to comparison >= on ints [JLS14:4.2.2] [JLS14:15.20.1].
Long-rem
Remainder & on longs [JLS14:4.2.2] [JLS14:15.17.3].
Long-mul
Multiplication * on longs [JLS14:4.2.2] [JLS14:15.17.1].
Long-less
Less-than comparison < on longs [JLS14:4.2.2] [JLS14:15.20.1].
Long-great
Greater-than comparison > on longs [JLS14:4.2.2] [JLS14:15.20.1].
Long-eq
Equality == on longs [JLS14:4.2.2] [JLS14:15.21.1].
Long-div
Division / on longs [JLS14:4.2.2] [JLS14:15.17.2].
Long-add
Addition + on longs [JLS14:4.2.2] [JLS14:15.18.2].
Int-neq
Non-equality != on ints [JLS14:4.2.2] [JLS14:15.21.1].
Int-mul
Multiplication * on ints [JLS14:4.2.2] [JLS14:15.17.1].
Int-lesseq
Less-than-or-equal-to comparison <= on ints [JLS14:4.2.2] [JLS14:15.20.1].
Int-great
Greater-than comparison > on ints [JLS14:4.2.2] [JLS14:15.20.1].
Int-eq
Equality == on ints [JLS14:4.2.2] [JLS14:15.21.1].
Int-and
Bitwise conjunction & on ints [JLS14:4.2.2] [JLS14:15.22.1].
Int-add
Addition + on ints [JLS14:4.2.2] [JLS14:15.18.2].
Long-sub
Subtraction - on longs [JLS14:4.2.2] [JLS14:15.18.2].
Int-sub
Subtraction - on ints [JLS14:4.2.2] [JLS14:15.18.2].
Int-rem
Remainder & on ints [JLS14:4.2.2] [JLS14:15.17.3].
Int-less
Less-than comparison < on ints [JLS14:4.2.2] [JLS14:15.20.1].
Int-div
Division / on ints [JLS14:4.2.2] [JLS14:15.17.2].
Long-plus
Unary plus + on longs [JLS14:4.2.2] [JLS14:15.15.3].
Long-not
Bitwise complement ~ on longs [JLS14:4.2.2] [JLS14:15.15.5].
Long-minus
Unary minus - on longs [JLS14:4.2.2] [JLS14:15.15.4].
Int-not
Bitwise complement ~ on ints [JLS14:4.2.2] [JLS14:15.15.5].
Int-minus
Unary minus - on ints [JLS14:4.2.2] [JLS14:15.15.4].
Int-plus
Unary plus + on ints [JLS14:4.2.2] [JLS14:15.15.3].