From Hoare Logic to Matching Logic

Matching logic has been recently proposed as an alternative program \nverification approach. \nUnlike Hoare logic, where one defines a language-specific proof system \nthat needs to be proved sound for each language \nseparately, matching logic provides a language-independent and \nsound proof system \nthat directly uses the trusted operational semantics of the language as axioms. \nMatching logic thus has a clear practical advantage: it eliminates the need for \nan additional semantics of the same language in order to reason about programs, \nand implicitly eliminates the need for tedious soundness proofs. \nWhat is not clear, however, is whether matching logic is as powerful as \nHoare logic. \nThis paper introduces a technique to mechanically translate Hoare logic proof \nderivations into equivalent matching logic proof derivations. \nThe presented technique has two consequences: first, it suggests that matching \nlogic has no theoretical limitation over Hoare logic; and second, it provides a new \napproach to prove Hoare logics sound.