Abstract.
Specifications and programs make much use of nondeterministic and/or partial expressions, i.e. expressions which may yield several or no outcomes for some values of their free variables. Traditional 2-valued logics do not comfortably accommodate reasoning about undefined expressions, and do not cater at all for nondeterministic expressions. We seek to rectify this with a 4-valued typed logic E4 which classifies formulae as either “true”, “false”, “neither true nor false”, or “possibly true, possibly false”. The logic is derived in part from the 2-valued logic E and the 3-valued LPF, and preserves most of the theorems of E. Indeed, the main result is that nondeterminacy can be added to a logic covering partiality at little cost.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Received July 1996 / Accepted in revised form April 1998
Rights and permissions
About this article
Cite this article
Morris, J., Bunkenburg, A. Partiality and Nondeterminacy in Program Proofs. Form Aspects Comput 10, 76–96 (1998). https://doi.org/10.1007/PL00003927
Issue Date:
DOI: https://doi.org/10.1007/PL00003927