An important distinction in Whiley is the difference between functions and a methods. In Whiley, functions have certain properties that ensure they behave more like mathematical functions. These properties are as follows:
- No Aliasing. Functions will only accept and manipulate variables of value type (i.e. all the primitive and used-defined types we’ve seen so far, but not the process types covered later). Thus, the notion of object aliasing is completely irrelevant when talking about functions.
- No Side-effects. Functions cannot have any form of side-effect which is visible outside of the function itself. This includes, for example, any form of I/O and, hence, functions may not read from disk, or print to an output stream.
In the parlance of programming language research, these properties give rise to the notion of pure functions. In constrast, methods in Whiley can have side-effects, such as reading files and writing to output streams (this is discussed in more detail later on). The reason for the having a strong distinction between functions and methods is to simplify the verification problem, and ensure only local reasoning is required for functions.