さっそく

落書きしてみた。Hoareのなんか（って何だよ）

圏論ってタグつけるほどのもんじゃないけど…

も少し書くと、これはモデルの抽象化の話を可換図式で書いてみたもの。Sがモデルの状態、αが抽象化。
具体的な世界で成り立つ論理式の帰結は、抽象化した世界での論理式の帰結を含意する。その関係図。

マジメに圏をこさえて考えるとすると、どうなるかなぁ。