Unifying Theories of Undefinedness
Woodcock Jim, Saaltink Mark, Freitas Leo · NATO science for peace and security series. D, Information and communication security · 2009
We propose a unifying theory of undefined expressions in logics used for formally specifying software systems. We show how to use classical logic to prove facts in a monotonic partial logic with guards, and we exhibit guards for several different semantical systems. We show how classical logic can be used to prove semi-classical facts. The mechanical theorem prover Z/Eves is used to prove facts about semi-classical Z specifications, although it uses classical logic; it does this with guards from McCarthy logic. It can also be used to prove facts about VDM specifications. The use of left-to-right guards guarantees, for example, that every theorem proved in Z/Eves is valid in VDM and in Z.