N The above notation states that we have a function called 'SQUARE'.
It accesses the external variable 'ns' which is here specified as a write ('wr') variable of the type dass, meaning that the operation may alter its value. The pre-condition states that the student 'n' should not already be a member of this dass. The post-condition states that the dass is changed by having the student's name added into it by the union operator. There are various things to note about this example. This operation does not return a result in the way that functions are compelled to.