A note on undefined expression values in programming logics (Q1093365)

In many programming logics, expressions of programming language are used as assertions of the formal system. The problem is that it is normally assumed in mathematical logic that the values of terms and formulas are always defined. This short note describes an approach whose main advantage is that verifications are almost identical to those that can be used when undefinedness cannot occur. The author says that it seems possible to allow undefinedness of expression values in program verification logics without resorting to unfamiliar formal systems, and further it is possible to transform the assertions that arise in the presence of undefinedness into formulas that are almost identical to those conventionally used.