Note: [] Address for correspondence: Department of Computer Engineering,
Sharif University of Technology, USA
Abstract: The abstraction inherent in most specifications and the need to
specify nondeterministic programs are two well-known sources of nondeterminism
in formal specifications. In this paper, we present a Z-based formalism by
which one can specify bounded, unbounded, erratic, angelic, demonic, loose,
strict, singular, and plural nondeterminism. To interpret our specifications,
we use a constructive set theory, called CZ set theory, instead of the
classical set theory Z. We have chosen CZ since it allows us to investigate the
notion of nondeterminism from the formal program development point of view. In
this way, we formally construct functional programs from Z specifications and
then probe the effects of the initially specified nondeterminism on final
programs. Our investigation shows that without specifying nondeterminism
explicitly, the effects of the nondeterminism involved in initial
specifications will not be preserved in final programs. We prove that using the
new formalism, proposed by this paper, for writing nondeterministic
specifications leads to programs that preserve the initially specified
modalities of nondeterminism.
Keywords: formal specification, formal program development, constructive Z, Martin-Löf's theory of types, nondeterminism, modalities of nondeterminism
