…アトリプル（あるいはホーア式）と呼ばれる表現を論理式とする論理です。事前条件と呼ばれる（通常の）論理式P、プログラムコードC、事後条件と呼ばれる論理式Qを組み合わせた {P}C{Q} がホーアトリプルです。その意味は： プログラムコードCの実行前の状態がPを満たしていたなら、プログラムコードCの実行後の状態はQを満たす。 プログラムの状態空間をS、プログラムコードCは状態空間の自己写像 S→S と解釈して、通常の古典論理の論理式に翻訳するなら： ∀x∈S.( P(x) ⇒ Q…

…定性写像の圏におけるホーア式のモデル 非決定性写像の圏におけるホーア式のモデル 踊り場・編 非決定性写像の圏におけるホーア式のモデル いちおう完結・編 クリーネ代数とはちょっと離れますが、ホーア論理の圏論的扱いについては： 真偽構造が付いた圏 -- ホーア論理のために ホーア論理の圏論的な定式化 インスティチューションとホーア論理 というわけで、クリーネ代数／テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を…

…は、実行文fに対するホーア式 p{f}q と似たようなものです。ガード演算は圏の結合（composition）と整合する必要があるので、次の条件も仮定します。 (f・q);g = f;(q・g) (f・q);(r・g) = (f・(q∧r));g これらを組み合わせると、(f・q);(r・g) = f;((q∧r)・g) も出ます。順次実行「;」、論理AND「∧」、ガード「・」が、ある程度は置き換え可能であることを示しています。論理OR「∨」と足し算「+」は、非決定性の分岐を…

…⊆P(f)(V) はホーア式 U{f}V です。ベキ集合のグロタンディーク構成により得られた全体圏は、ホーア式を射とする圏とみなすことができて、ファイブレーション射影は、ホーア式にその制約記述の対象であるプログラムを対応させます。全体圏における結合は、2つのホーア式を前提とする含意の推論（カット規則）です。最近、デイヴィッド・スピヴァック（David I. Spivak）は、データベースの定式化にインデックス付き圏（あるいは前層）を使う方法を開発しています。スピヴァックのデー…

…記述の具体例として、ホーア式やメイヤーの契約があります。値のあいだの個別の関係 b = f(a) という形ではなくて、入力の範囲となる集合Aと出力の範囲となる集合Bが与えられます。そして、「x∈A ならば f(x)∈B」という論理的主張によって法則が記述されます。もちろん、法則の記述は複数の論理的主張（表明）を使ってもかまいません。番号1, 2, ... に対する「x∈A1 ならば f(x)∈B1」、「x∈A2 ならば f(x)∈B2」、… のような形です。具体的に与えられた…

…., αn, β がホーア式（ホーア論理の論理式）だとして、α1, α2, ..., αn |- β とは、「α1, α2, ..., αn を仮定してβが証明できる」ことです。あるいは、「単一の論理式 α1∧α2∧ ... ∧αn を仮定してβが証明できる」と言っても同じです。ホーア式の集合Tが次の性質を持つときセオリーと呼びます*1。 α1, α2, ..., αn ∈T、α1, α2, ..., αn |- β ならば、β∈T 。 つまり、セオリーとは証明に関して閉じて…

…の記事で取り上げた、ホーア式のモデルや正規言語の話のなかでもベキ等半環が出てきます。 非決定性写像の圏におけるホーア式のモデル 正規表現とオートマトン：イプシロン指標 （イプシロン指標はベキ等半環の準同型） そういえば、HTTPメソッドにさえベキ等概念は登場しますよね。 訂正補足：HTTPメソッド、URL、そして標準化された動詞 ベキ等性はまた、正規化や観測の概念につながります。（ただし、足し算というより掛け算です。） ベキ等、正規化、計算、射影、観測 計算（computat…

…由に書けるので、コミュニケーションが非常にスムーズになります。背景となる理屈は次の記事に書いてありますが、もちろん、使うためにこんな理屈を知る必要はありません。 非決定性写像の圏におけるホーア式のモデル いちおう完結・編 *1:[追記] FitNesseとCatyFITの構文や操作性は別物です。まったく互換性はありません。アイディアと基本的な構造だけ、FIT/FitNesseから拝借しています（「FIT/FitNesseにインスパイアされた」と言えばいいのかな？）。[/追記]

…定性写像の圏におけるホーア式のモデル - 檜山正幸のキマイラ飼育記 (はてなBlog) 非決定性写像の圏におけるホーア式のモデル 踊り場・編 - 檜山正幸のキマイラ飼育記 (はてなBlog) 続き＆完結。内容： アブラムスキー達の仕様構造 メイヤーのCommandとQuery（教えに背く） メイヤーの契約（教えを省く） エクスペクテーション エクスペクテーションの実行 エクスペクテーション・ベースのホーア式 純粋なホーア式とエクスペクテーション FITスタイルの記述 インター…

…定性写像の圏におけるホーア式のモデル」にて： この記事で導入した概念を使ってエクスペクテーションのモデルを構成するのは次回（続き）にします。次回（続き）では、条件と実行文をあまり区別しない方法を紹介します。エクスペクテーションの定式化では、条件と実行文を区別しません。 と書いたのですが、先に進む前に、前回の補足説明とか言い残した事とかを書いておきます。階段で上の階に上がる途中の踊り場みたいなもの、ということで「踊り場・編」。内容： 前回の復習 理解しにくいところ、誤解しやすい…

…と順序 ガード演算 ホーア式 等式的な表現 まとめと予告 全体： 非決定性写像の圏におけるホーア式のモデル 非決定性写像の圏におけるホーア式のモデル 踊り場・編 非決定性写像の圏におけるホーア式のモデル いちおう完結・編 非決定性写像の圏プログラムの挙動は状態遷移で表現できますが、決定性の遷移だけだと何かと不便なので、非決定性遷移を使うことにしましょう。S, Tが集合のとき、fがSからTへの非決定性写像だとは、通常の写像としては f:S→Pow(T) と書けることです。Pow…

ホーア論理、ホーア式については何度か触れたことがあります（例えば、「デュアルプログラミングとエクソシストゲーム」、「極小プログラミング言語とホーア論理」）。ホーア式（ホーア論理における論理文）を記述する構文と実行フレームワークがあると便利そうです。ホーア式というと、その用途として単体テスト／振る舞い記述が思い浮かびますが、その他の用途でも意外に広く適用できるような気がしてきました。まず構文ですが、JavaScriptやJSON構文を参考にした簡単なものにします。構文上は、明確…

…能であること*1を、ホーア式を使って構文的に定義しましょう（ホーア式に関しては「極小プログラミング言語とホーア論理」とか、https://m-hiyama.hatenablog.com/search?q=ホーア式 から適当に拾って見てください）。まず、単純文を次のように定めます。 post(x);は単純文。postの引数はリテラルか変数。 yをY型の変数としてy = get();（代入文）は単純文。 いくつかの変数x1, x2, ... のあいだの等式（例えば、x1 == x…

…はあります。内容： ホーア式 ホーア式の正しさ プログラムの証明 こんなにめんどくさい なにが重要か ●ホーア式ホーア論理の式（ホーア式とか、ホーア・トリプルと呼ばれる）は、プログラムの文と仕様記述を一緒にしたようなものです。p, qが論理式（条件）でSが文だとして、p{S}q という形で書きます。中括弧の使い方が逆である {p}S{q} が一般的かと思いますが、僕は p{S}q を使ってますね。理由： 多くのプログラミング言語では、文を囲むために中括弧を使っている。 ホーア…

…グ言語をうんと小さくするのは、ライブラリのほうにフォーカスしたいからなんです（僕の動機は）。ライブラリが使いやすくリッチだったら言語能力が貧弱でもなんとかなるような気がします。その「気がします」という感覚を確かめてみたいんです。それと、これくらい単純だと、ブール代数とクリーネ代数の算術的計算*1だけで意味論が作れるし、ホーア式での検証も（がんばれば）できなくもないですね。ようするにオモチャとしては遊びやすいシロモノだってことです。 *1:より正確にはHorn論理式の範囲の計算

…の型理論入門」参照、ホーア式には明示的含意「==>」を入れている）。次は、設計プログラム＝形式仕様の（毎度お決まりの）例です。 spec IntStack { interface { new(); // コンストラクタ仕様も記述できるとする // @Accessorは副作用がないことを意味する @Accessor int top(); @Accessor; boolean isEmpty(); void push(int x); void pop(); } // 制約[1]に…

…契約に限らず、一般のホーア式もプログラムコードに翻訳する方法を考えてみました。特に、全称限量子（「すべての…に関して…」を意味する）の扱いを工夫してみます。（これは、「AspectJによる契約駆動開発」に関連したエントリーです。）明示的な含意記号契約とホーア式は似てるけどわずかに違う、と言いました。例えば、「事前条件：x > 0、実行文：f(x);、事後条件：result >= 15」の3つ組を考えて： 契約としての解釈：x > 0 が成立しないなら、契約が破られている。 ホ…

…では「だ・である」調ホーア式と契約ホーア式（ホーア表明、ホーア制約）は、「事前条件P、実行文E、事後条件Q」の三つ組み（トリプル）で、通常は {P}E{Q}の形で書かれる。だけど僕は、P{E}Qの形を使っている。ブレイス（中括弧、波括弧）を使った理由はおそらく、（Pascalなどで）ブレイスがコメントだったからだろうけど、今じゃブレイスはブロックを意味する言語が多いから、P{E}Qのほうが自然に見えるので。ところがですね、メイヤー本『招待』(9.4.4)によると、トニー・ホー…

…明”とは仕様記述言語（または制約記述言語）レベルの証明で、古典的な“プログラムの証明”とはどうもストレートに結びつかないのです。プログラムの証明は、厳密なソースコードレビューみたいなもんだけど、ソースコードに対応するフォーマルな概念が見あたらないのね。だから、ソースレベルの変換とか合成とかを記述すべき場所が分からない。ホーア式のような形でSenΣのなかにソース断片を押し込めるけど、なんか気色悪いよ。で、「ソースコード（構文的対象）に対応する圏論的概念てなによ？」が最近の疑問。

… + 1」ですから、ホーア式では (value() == n){inc();}(value() == n + 1) です。が、変数nの扱いが難しい。論理（学）の言葉でいえば、nは、for all n として使われる束縛変数ですから、制約全体の意味は： どんなnに対しても 「value()の値が n ならば、 inc(); の後では、 value() == n + 1」 となる。となります。「どんなnに対しても」だから、いろいろな値を片っ端からnに入れてテスト、ってのはバカバカ…

…な記述文（の構文）はホーア式でしょう。事前条件P、実行部E、事後条件Qを組み合わせて {P}E{Q} という形で書きますが、現在のプログラミング言語との相性からは、中括弧の使用法を逆にして P{E}Q がいいと僕は思います（ので、こっちを使います）。P{E}Q の意味は、「条件Pを満たしている状態で、Eを実行したら、実行後には条件Qを満たす」というものです。例えば、 (value() >= 0){inc();}(value() > 0) ならば、「value()が0以上の状態…