極小プログラミング言語とホーア論理 - 檜山正幸のキマイラ飼育記 (はてなBlog)一昨日定義した極小プログラミング言語を、TTPL（Tiny Toy Programming Language）というツマンネー名前で呼ぶことにします。 んでまー、TTPLをああいう仕様にしたのは、ホーア論理を直接的に使いたい、という理由があります。つうわけで、ホーア論理をTTPLを使って説明します。ただし、最初に言っておきますが、僕は（ホーア論理のような）プログラム証明を推奨する気はありません（どっちかいうと反対派）。それでも、理屈は知っておかないと、それから先に進めないってことはあります。 内容： ホーア式 ホーア式の正しさ プログラムの証明 こんなにめんどくさい なにが重要か ●ホーア式 ホーア論理の式（ホーア式とか、ホーア・トリプルと呼ばれる）は、プログラムの文と仕様記述を一緒にしたようなものです。p, qが論理式（条件）でSが文だとして、p{S}q という形で書きます。中括弧の使い
