For example, a class "PERSON" represents the members of a group and
has the attributes his/her lastname, firstname, telephone numbers and the
number of a card to access buildings. The operations "ChangeLastname",
"Change-Firstname", "ChangeTel", "ChangeCardnb", "AddPerson" and "Remove-Person"
are generated automatically by RoZ. The specification of these operations
is contained in their form. For instance, let us consider "ChangeLastname"
which allows to modify the last name of a person. In the "Details" tab,
the operation has an argument "newlastname" which is the input parameter
of the operation. The "Semantics" field contains the key-word intension
operation which signifies that "ChangeLastname" is an operation on
the attributes of the class. In the "PostConditions" tab, the post condition
of the operation is written as a Z Latex type : it means that the new value
of the attribute "lastname" is the argument of the operation "newlastname"
and that the others attributes of "PERSON" are unchanged by the operation.