A logic covering undefinedness in program proofs (Q790610)

There is a growing literature on proving that programs satisfy their specifications. Most methods employ propositional and predicate calculus. Such logical systems do not reflect the possibility of ''undefined values''. However, recursive definition often results in partial functions and iteration gives rise to programs that may fail to terminate for some inputs. This paper provides and demonstrates a logic in which the logical operators give defined results even if no value is known for some of their operands. It is claimed that this logical system is useful in program proofs.