======================================
B_ATTRIBUTES (invariant admissibility)
Successfully verified.
======================================
B_ATTRIBUTES.default_values_for_attribute (creator)
Successfully verified.
======================================
B_ATTRIBUTES.attribute_initialization
Successfully verified.
======================================
B_ATTRIBUTES.attribute_assignment
Successfully verified.
======================================
B_ATTRIBUTES.argument_assignment
Successfully verified.