With traditional Hoare logic it is possible to prove partial correctness of programs through statements of the kind "If the precondition holds and the program terminates, then the postcondition holds." In this work-in-progress we try to extend Hoare logic in a way that it can deal also with crashes (i.e., abrupt termination).
Let us consider as example a program fragment P which consists of the assignment to an undefined expression x:= 1/0. Let us assume furthermore that the underlying logic is two-valued and total, and evaluates expressions like 1/ 0=0 to false.
The Hoare triple (|1/ 0 =/= 0|) x:= 1/0 (|x =/= 0|), which is an instance of the \it assign axiom-schema, can be weakened (by the weakening rule) to the valid Hoare triple (|true|) x:= 1/0 (|x =/= 0|). The last expression looks as if we could without precondition get the postcondition x =/= 0 directly from the program P under the assumption that P terminates. Hence it is important to note that in this context "termination" means also that the program does not crash. That is, we should read the semantics of a valid Hoare triple more accurately as "If the precondition holds, the program terminates and does not crash, then the postcondition holds."
We propose to extend the two-valued logic to a three-valued logic, in which the third truth value corresponds to "crash." In such an extension it would be possible to model partial functions in programs by partial functions in the extended Hoare logic.
We aim to discuss choices about possible three-valued logic candidates, and to relate this approach to Kleene algebras, in the perspective of using algebraic expressions inside programs as effective tools to directly calculate partial correctness assertions.