主要观点：作者尝试理解在为 Hoare 三元组赋予语义时切换⊆和⊇的影响，提及 Yann Herklotz 指出 Patrick Cousot 的 POPL 2024 论文做了相关内容，本文旨在得到类似 Cousot 的图但保持简单。假设存在状态集，命令是状态上的二元关系，定义了“最强后置条件”函数 sp 来给 Hoare 三元组赋予语义，有八种关于 Hoare 三元组的解释，包括部分正确性、反向 Hoare 逻辑、必要先决条件等，可将它们组装成“Hoare 立方体”，通过实线和虚线连接表示相等和等价语义，还提到了一些相关工作和参考文献。
关键信息：

• 定义了命令与状态的关系及相关概念。
• 给出 Hoare 三元组的不同解释及 sp 函数的定义。
• 介绍“Hoare 立方体”及各种语义之间的关系。
• 提及相关研究工作及参考文献。
  重要细节：
• 详细说明了各种语义的具体形式及区别，如 may、must、forward、backward、over、under 等的含义。
• 解释了立方体中实线和虚线连接的意义及相关等式和双射关系。
• 提及不同研究中对各种逻辑的定义和研究情况，如 Möller 等、Zilberstein 等、Ascari 等的工作。
• 指出 Zhang 和 Kaminski 表格中的一些潜在混淆点。