查看文章

Specification of system requirements is often involved with ambiguity and nondeterminism. Formal methods tend to mitigate ambiguity but nondeterminism remains as an inherent part of specification. This is due to the abstraction from real world details that causes a formal specification to define several results as a correct solution to a problem. Hence, a support for nondeterminism should be foreseen in formal methods.

In this paper, after studying different types of nondeterminism, some basic notations, namely multi-and power-schema, are added to Z formal language, to help explicit specification of nondeterminate constructs. Afterwards, a transformation is defined to generate nondeterministic semantics from specification in the same language. The results of adding the proposed notations is discussed from program development point of view.