Before revision: Applications Matching logic is used by the K Framework to define operational semantics and use themas a Hoare logic.
After revision: Applications Matching logic is used by the K Framework to specify an operational semantics and , from them, to createwith reachability logic a Hoare logic.