|
|
||
|
There are three places in the model where data objects can be defined:
This chapter describes the first kind of data, the other two (locals and parameters) are explained in the chapter devoted to operations.
Package-level data allow to retain state between operation invocations and for this reason are essential in a wide range of practical systems, even though they might be neglected in simple examples that are concerned with one-off value processing.
Data objects are defined in a way that is analogous to the definition of data types:
Data objects can have any of the types that are already known in the model - both standard types and user-defined types can be used and as seen above, types defined in other packages need to be fully-qualified.
Multiple data objects can be defined in a single invocation of defineDataObjects, but there is no need to define all package data in a single step - further data objects can be added to the package and objects can be redefined as well, although redefinition is signalled with a warning message:
It is not possible to remove a data object that was already defined in the given package - if there is a need to do so, the package has to be reconstructed (in a newly created model) without the unwanted data object.
Data objects are visible in the same package without qualification, although full qualification can still be used for readability. When accessed from other packages, data object names need to be fully qualified:
Similarly to data types (and consequently for all other names), package-level data object names are visible from all packages within the same model - there is no concept of “private” package data.
Since data objects have conceptually infinite lifespan and exist before any operation is invoked, they are considered to be always initialized with values that are valid for their types, although the means of actual initialization are outside of scope of FMT - it is not even possible to provide the initial value in the model. In other words, the initialization state is not tracked for package data (unlike local variables), which makes the user responsible to ensure that package data are indeed properly initialized in the actual system, before any modeled operation is invoked. The rationale for this simplification is that formal methods are rarely (if ever) used to construct complete systems together with their startup routines - instead, formal methods are typically used in a constrained scope, where the execution context is already established by the environment or some existing startup services. Still, even though the simplification can be justified, it is important for the user to be aware that there are no checks for the validity of initial state of package data.
Previous: Data types, next: Operations
See also Table of Contents.