[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,
enrich
int2bits
with
functions bitsand : bitlist × bitlist → bitlist;
bitsxor : bitlist × bitlist → bitlist;
bitsor : bitlist × bitlist → bitlist;
band : int × int → int;
comment: bitwise and;
bxor : int × int → int;
comment: bitwise xor;
bor : int × int → int;
comment: bitwise or;
bcompl : int → int;
comment: bitwise complement, !;
cast : int × int → int;
comment: cast(i, j): keep only last i bits of j, i.e.
cast(8, j) = (byte)j, cast(16, j) = (short)j.
See cast-if for an algebraic characterization.
;
. << . : int × int → int;
comment: generic left shift (no restriction on shift distance).;
. >> . : int × int → int;
comment: generic right shift (no restriction on shift distance).;
>>> : nat × int × int → int;
comment: generic zero right shift:
>>>(n, i, j) assume bit rep length of n for i and
shift by j (no restriction on j).;
. i<< . : int × int → int;
comment: i i<< j: If the promoted type of the left-hand operand is int,
only the five lowest-order bits of the right-hand operand are used as
the shift distance. It is as if the right-hand operand were subjected
to a bitwise logical AND operator & (⟧15.21.1) with the mask value
0x1f. The shift distance actually used is therefore always in the
range 0 to 31, inclusive. At run time, shift operations are performed
on the two's complement integer representation of the value of the left
operand.
The value of n<<s is n left-shifted s bit positions, this is equivalent
(even if overflow occurs) to multiplication by two to the power s.;
. i>> . : int × int → int;
comment: The value of n>>s is n right-shifted s bit positions with
sign-extension. The resulting value is ⌊n / 2^s⌋. For nonnegative
values of n, this is equivalent to truncating integer division, as
computed by the integer division operator /, by two to the power s.;
. i>>> . : int × int → int;
comment: The value of n>>>s is n right-shifted s bit positions with
zero-extension. If n is positive, then the result is the same as that
of n>>s, if n is negative, the result is equal to that of the expression
(n>>s)+(2<<~s) if the type of the left-hand operand is int, and to the
result of the expression (n>>s)+(2L<<~s) if the type of the left-hand
operand is long. The added term (2<<~s) or (2L<<~s) cancels out the
propagated sign bit. (Note that, because of the implicit masking of
the right-hand operand of a shift operator, ~s as a shift distance is
equivalent to 31-s when shifting an int value and to 63-s when shifting
a long value.);
. l<< . : int × int → int;
comment: long shift, uses mask value 0x3f instead of 0x1f, otherwise as i<<.;
. l>> . : int × int → int;
comment: long shift, uses mask value 0x3f instead of 0x1f, otherwise as i>>.;
. l>>> . : int × int → int;
comment: long shift, i.e. first arg is treated as a
long, and the mask value is 0x3f.
See description of i>>>;
axioms band-def : ⊦ band(i, j) = bits2int(bitsand(int2bits(i), int2bits(j)));
used for: ls;
bxor-def : ⊦ bxor(i, j) = bits2int(bitsxor(int2bits(i), int2bits(j)));
used for: ls;
bor-def : ⊦ bor(i, j) = bits2int(bitsor(int2bits(i), int2bits(j)));
used for: ls;
bcompl-def : ⊦ bcompl(i) = bits2int(bitsinvert(int2bits(i)));
used for: ls;
bitsand-onel : ⊦ bitsand(true ', bits + boolvar ') = bits + boolvar;
used for: ls;
bitsand-oner : ⊦ bitsand(bits + boolvar ', true ') = bits + boolvar;
used for: ls;
bitsand-zerol : ⊦ bitsand(false ', bits + boolvar ') = false ';
used for: ls;
bitsand-zeror : ⊦ bitsand(bits + boolvar ', false ') = false ';
used for: ls;
bitsand-rec
: ⊦ bitsand(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ')
= bitsand(bits + boolvar, bits0 + boolvar1) + (boolvar0 ∧ boolvar2);
used for: ls;
bitsxor-onel : ⊦ bitsxor(true ', bits + boolvar ') = bitsinvert(bits + boolvar);
used for: ls;
bitsxor-oner : ⊦ bitsxor(bits + boolvar ', true ') = bitsinvert(bits + boolvar);
used for: ls;
bitsxor-zerol : ⊦ bitsxor(false ', bits + boolvar ') = bits + boolvar;
used for: ls;
bitsxor-zeror : ⊦ bitsxor(bits + boolvar ', false ') = bits + boolvar;
used for: ls;
bitsxor-rec
: ⊦ bitsxor(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ')
= bitsxor(bits + boolvar, bits0 + boolvar1) + (¬(boolvar0 ↔ boolvar2));
used for: ls;
bitsor-onel : ⊦ bitsor(true ', bits + boolvar ') = true ';
used for: s, ls;
bitsor-oner : ⊦ bitsor(bits + boolvar ', true ') = true ';
used for: s, ls;
bitsor-zerol : ⊦ bitsor(false ', bits + boolvar ') = bits + boolvar;
used for: s, ls;
bitsor-zeror : ⊦ bitsor(bits + boolvar ', false ') = bits + boolvar;
used for: s, ls;
bitsor-rec
: ⊦ bitsor(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ')
= bitsor(bits + boolvar, bits0 + boolvar1) + (boolvar0 ∨ boolvar2);
used for: ls;
cast-def : ⊦ cast(i, j) = bits2int(lastn(i→n(i), fillsgn(i→n(i), int2bits(j))));
shiftleft : ⊦ i << j = bits2int(int2bits(i) + mklist(false, i→n(j)));
shiftrsign : ⊦ i >> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(j)) + int2bits(i)));
shiftrzero-def : ⊦ >>>(n, i, j) = bits2int(sublist(0, # fillsgn(n, int2bits(i)), mklist(false, i→n(j)) + fillsgn(n, int2bits(i))));
intshiftleft : ⊦ i i<< j = bits2int(int2bits(i) + mklist(false, i→n(band(j, 31))));
intshiftrsign : ⊦ i i>> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(band(j, 31))) + int2bits(i)));
intshiftrzero-def
: ⊦ i i>>> j = bits2int(sublist(0, # fillsgn(32, int2bits(i)), mklist(false, i→n(band(j, 31))) + fillsgn(32, int2bits(i))));
comment: this axiom uses 32 as a constant, i.e. it can be used only for integer shifts.
Use l>>> for long shifts.;
longshiftleft : ⊦ i l<< j = bits2int(int2bits(i) + mklist(false, i→n(band(j, 63))));
longshiftrsign : ⊦ i l>> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(band(j, 63))) + int2bits(i)));
longshiftrzero-def
: ⊦ i l>>> j = bits2int(sublist(0, # fillsgn(64, int2bits(i)), mklist(false, i→n(band(j, 63))) + fillsgn(64, int2bits(i))));
comment: this axiom uses 64 as a constant, i.e. it can be used only for long shifts.
Use i>>> for integer shifts.;
end enrich