When creating an attribute, it is common that you will also need a set-procedure for it. For example, for attribute property you need a procedure set_property to set it. This feature takes one argument of the same type as property or is anchored to it. The only thing you have to do with the feature wizard is check the button Generate set procedure.

The feature that is generated in addition to the attribute itself is placed in feature clause Element change and is exported to all classes. If you have selected or entered an invariant, the precondition will protect this invariant. Example of a generated set-procedure:

feature -- Element change set_button (a_button: EV_BUTTON) -- Assign `a_button' to `button' require a_button_not_void: a_button /= Void do button := a_button ensure button_assigned: button = a_button end