A Practical Approach to Partial Functions in CVC Lite
Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik,
Arie Gurfinkel, and David L. Dill (PDPAR'04)
Most verification approaches assume a mathematical formalism in which
functions are total, even though partial functions occur naturally in
many applications. Furthermore, although there have been various
proposals for logics of partial functions, there is no consensus on
which is ``the right'' logic to use for verification applications. In
this paper, we propose using a three-valued Kleene logic, where
partial functions return the ``undefined'' value when applied outside
of their domains. The particular semantics are chosen according to
the principle of least surprise to the user; if there is
disagreement among the various approaches on what the value of the
formula should be, its evaluation is undefined. We show that the
problem of checking validity in the three-valued logic can be reduced
to checking validity in a standard two-valued logic, and describe how
this approach has been successfully implemented in our tool, CVC Lite.