There are several FM based on set theory and first-order logic (e.g. Z [1]}, VDM [2]}, B [3]}). These notations are designed to write large, complex specifications; and there is a number of tools to work with them such as editors, typecheckers, theorem provers, animators, etc. However, in this paper we will use the plain and simple language of mathematics extended with a couple of conventions, to avoid explaining the peculiarities of a particular notation. This will be enough as to show the `look-and-feel' of such specifications.
