class BIT_STRING

Features exported to ANY

Long and very long bit sequences. An INTEGER index can be used to access each bit of the sequence. The leftmost bit has index 1 and the rightmost bit has index count.

For short bit sequences (less or equal to 32 or 64), also consider to use basic INTEGER_N type.

Direct parents

conformant parents

TRAVERSABLE

non-conformant parents

PLATFORM

Summary

creation features

exported features

 Rotating and shifting:
 Bitwise Logical Operators:

Conversions:

Others:

Other features:

Details

make (n: INTEGER)

Make bit sequence of n bits. All bits are set to False.

require

  • n > 0

ensure

  • count = n
  • all_default

from_string (model: STRING)

Create or set Current using model which is supposed to be a sequence of mixed 0 or 1 characters.

require

  • model.is_bit

count: INTEGER
 Number of bits in the sequence.

ensure

  • definition: Result = upper - lower + 1

lower: INTEGER

Minimum index.

See also upper, valid_index, item.

upper: INTEGER

Maximum index.

See also lower, valid_index, item.

is_empty: BOOLEAN

Is collection empty ?

See also count.

ensure

  • definition: Result = (count = 0)

make (n: INTEGER)

Make bit sequence of n bits. All bits are set to False.

require

  • n > 0

ensure

  • count = n
  • all_default

from_string (model: STRING)

Create or set Current using model which is supposed to be a sequence of mixed 0 or 1 characters.

require

  • model.is_bit

valid_index (idx: INTEGER): BOOLEAN

True when index is valid (ie. inside actual bounds of the bit sequence).

ensure

  • definition: Result = (lower <= idx and idx <= upper)

item (idx: INTEGER): BOOLEAN
 True if idx-th bit is 1, False otherwise.

require

  • valid_index(idx)

first: BOOLEAN

The very first item.

See also last, item.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: BOOLEAN

The last item.

See also first, item.

require

  • not is_empty

ensure

  • definition: Result = item(upper)

put (value: BOOLEAN, idx: INTEGER)
 Set bit idx to 1 if value is True, 0 otherwise.

require

  • valid_index(idx)

ensure

  • value = item(idx)

put_1 (idx: INTEGER)
 Set bit idx to 1.

require

  • valid_index(idx)

ensure

  • item(idx)

put_0 (idx: INTEGER)
 Set bit idx to 0.

require

  • valid_index(idx)

ensure

  • not item(idx)

shift_by (n: INTEGER)

Shift n-bits.

 n > 0 : shift right,
 n < 0 : shift left,
 n = 0 : do nothing.
Falling bits are lost and entering bits are 0.
|*** PR(17/10/2004) change entering into incoming? (everywhere)

ensure

  • count = old count

shift_left_by (n: INTEGER)

Shift left by n bits. Falling bits are lost and entering bits are 0.

require

  • n >= 0

shift_right_by (n: INTEGER)

Shift right by n bits. Falling bits are lost and entering bits are 0.

require

  • n >= 0

rotate_by (n: INTEGER)

Rotate by n bits.

 n > 0 : Rotate right,
 n < 0 : Rotate left,
 n = 0 : do nothing.

rotate_left_by (n: INTEGER)
 Rotate left by n bits.

require

  • n >= 0

rotate_right_by (n: INTEGER)

Rotate right by n bits.

require

  • n >= 0

^ (s: INTEGER): BIT_STRING

Sequence shifted by s positions (positive s shifts right, negative left; bits falling off the sequence's bounds are lost). See also infix "|>>" and infix "|<<".

require

  • s.abs < count

|>> (s: INTEGER): BIT_STRING

Sequence shifted right by s positions. Same as infix "^" when s is positive (may run a little bit faster).

require

  • s > 0

|<< (s: INTEGER): BIT_STRING

Sequence shifted left by s positions. Same as infix "^" when s is negative (may run a little bit faster.

require

  • s > 0

# (s: INTEGER): BIT_STRING

Sequence rotated by s positions (positive right, negative left).

require

  • s.abs < count

#>> (s: INTEGER): BIT_STRING

Sequence rotated by s positions right.

require

  • s >= 0
  • s < count

#<< (s: INTEGER): BIT_STRING

Sequence rotated by s positions left.

require

  • s >= 0
  • s < count

and (other: BIT_STRING): BIT_STRING
 Bitwise and of Current with other

require

  • count = other.count

ensure

  • Result.count = Current.count

implies (other: BIT_STRING): BIT_STRING

Bitwise implication of Current with other

require

  • count = other.count

ensure

  • Result.count = Current.count

not: BIT_STRING

Bitwise not of Current.

ensure

  • Result.count = Current.count

or (other: BIT_STRING): BIT_STRING

Bitwise or of Current with other.

require

  • other /= Void
  • count = other.count

ensure

  • Result.count = Current.count

xor (other: BIT_STRING): BIT_STRING

Bitwise xor of Current with other

require

  • other /= Void
  • count = other.count

ensure

  • Result.count = Current.count

and_mask (other: BIT_STRING)

Apply bitwise and mask of other onto Current.

require

  • count = other.count

implies_mask (other: BIT_STRING)

Aply bitwise implies mask of other.

require

  • count = other.count

or_mask (other: BIT_STRING)

Apply bitwise or mask of other onto Current.

require

  • count = other.count

xor_mask (other: BIT_STRING)

Apply bitwise xor mask of other onto Current

require

  • count = other.count

invert

Invert Current bit-per-bit.

to_string: STRING

String representation of bit sequence. A zero bit is mapped to '0', a one bit to '1'. Leftmost bit is at index 1 in the returned string.

 Note: see append_in to save memory.

ensure

  • Result.count = count

to_integer: INTEGER

The corresponding INTEGER value when count <= Integer_bits. No sign-extension when count < Integer_bits.

require

    all_cleared: BOOLEAN
     Are all bits set to 0?
    
    all_default: BOOLEAN
     Are all bits set to 0?
    
    clear_all

    Set all bits to 0

    ensure

    • all_default

    all_set: BOOLEAN
     Are all bits set to 1?
    
    set_all

    Set all bits to 1

    ensure

    • all_set

    is_equal (other: BIT_STRING): BOOLEAN

    Is other attached to an object considered equal to current object ?

    require

    • other /= Void

    ensure

    • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

    copy (other: BIT_STRING)

    Update current object using fields of object attached to other, so as to yield equal objects. Note: you can't copy object from a different dynamic type.

    require

    • same_dynamic_type(other)

    ensure

    • is_equal(other)

    out_in_tagged_out_memory
     Append terse printable represention of current object
     in tagged_out_memory
    

    ensure

    • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
    • append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))

    append_in (str: STRING)

    Append in str a viewable representation of Current.

    set_from_string (model: STRING, offset: INTEGER)

    Use the whole contents of model to reset range offset .. offset + model.count - 1 of Current. Assume all characters of model are 0 or 1.

    require

    • model.is_bit
    • valid_index(offset)
    • valid_index(offset + model.count - 1)

    ensure

    • count = old count

    get_new_iterator: ITERATOR [E_][BOOLEAN]

    Class invariant