+
Point of view
All features
class PACKRAT_CHOICE
is_equal (other: PACKRAT_CHOICE):
BOOLEAN
effective function
require
ensure
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
copy (other: PACKRAT_CHOICE)
effective procedure
require
- not immutable
- same_dynamic_type(other)
- not immutable
- same_dynamic_type(other)
- not immutable
- same_dynamic_type(other)
ensure
require
-
locked: tagged_out_locked
-
locked: tagged_out_locked
-
locked: tagged_out_locked
ensure
-
still_locked: tagged_out_locked
-
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))
require
ensure
- not Result.is_equal(yes) implies context.buffer.current_index = old context.buffer.current_index
require
- first /= Void
- second /= Void
ensure
frozen
effective function
{}
ensure
-
good_hash_value: Result >= 0
frozen
effective function
frozen
effective function
frozen
effective function
require
ensure
- not Result.is_equal(yes) implies context.buffer.current_index = old context.buffer.current_index