Set-procedure
When creating an attribute, it is common that you will also need a set-procedure for it. For example, for attribute
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