An Approach to Nondeterminism in Translation of CZ Set Theory into Martin-Löf 's Theory of Types

Due to the high level of abstraction involved in formal specification of software systems, nondeterminism comes as an inevitable part of formal specifications. Therefore, support for nondeterminism should be provisioned in developing programs from their formal specifications. In this paper, an existing translation of CZ set theory into Martin-Löf's theory of types is extended to consider nondeterministic specifications in CZ language.