Access Modes of External Functions

In order to allow different kinds of accesses to external entities, external functions can be declared either as ``monitored'' or as ``output'' functions. In the first case, the external function can be read, but not written (e.g user input), in the second case, the external function can be written, but not read (e.g. output channels like stdout and stderr).

As a restriction, an external function can be either a monitored or an output function, not both. If a function would have both modes, reasoning about the values of that function would require special case distinctions: If a location of such a function is updated in one step of the ASM by means of an update rule, it cannot be guaranteed that the location has the updated value in the next step, because the environment might have changed it in the meantime.

In the following example, the 0-ary function error is defined as an external function with ``output'' access mode; it is used in the parent asm for displaying an error message on ``stderr'' and for setting an ok_flag to false.

The value that is used for updating the external function can be accessed using the named result parameter msg. The use construct includes pre-defined header files containing function declaration that are in this case used to declare the external functions stdout, stdin, and stderr.

If no access mode is specified in the declaration of an external function, the mode ``monitored'' is assumed.