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

…定性写像の圏におけるホーア式のモデル いちおう完結・編 - 檜山正幸のキマイラ飼育記 にて： 実行ログとは、それぞれのエクスペクテーション実行により得られた事後状態s'、戻り値y、成功・失敗の別rの組(s', y, r)を並べたものです。（注：実際には、状態を完全に記録するのは困難です。ここは概念的な話です。）...[snip]...実用の観点からは、実行ログが最も重要な成果物となります。 この点を少し補足：エクスペクテーションの実行結果は、後でレポートする必要があるので、エ…

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

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

…ペクテーションの列、ホーア・トリプルです。これらは、次の形でWiki文書として記述されます。 構文要素 Wiki記法 エクスペクテーション テーブルの1行 エクスペクテーションの列 テーブル ホーア・トリプル 見出しで識別された3つのセクション トリプルは、事前条件、実行部、事後条件の3つの部分からなりますが、事前条件と事後条件は省略可能です。条件が省略されていても、常に真となる条件がそこにあると思えば「トリプル（三つ組）」です。さて、エクスペクテーションは、論理式と実行文を…

…です。○○の部分は、ホーア論理に基づくアサーションとか契約（コントラクト）です。防衛コードを書く労力を、アサーション／契約のほうに振り向けてね、っと。アサーション／契約をちゃんと書くようになれば、自然にどうでもいい防衛コードは書かなくなるでしょう。ですから、スローガンを「アサーション／契約を書こう」に変更すればいいんでしょうが、アサーション／契約のサポート状況があんまり芳しくない。単体テストツールの類は普及してますが、楽しく使っている人は一部でしょう。実際、楽しくないかもしれ…

…すべての原点といえばホーア論理です。ホーア論理のスタイルにより、Catyスクリプトのための演繹系を定義します。これは、インタプリタのみならずコマンドやファシリティの、仕様記述とテストの枠組みを与えます。念のため注意しておきますと； ホーア論理は「枠組みを与えます」が、機械的推論アルゴリズムに向いているとは言えません。アルゴリズムはまた別に考える必要があります。内容： ホーア・トリプル 基本的な式に関する推論規則 包含関係式に関する推論規則 式の構成に沿った推論規則 簡単な派生…

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

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

…いう仕様にしたのは、ホーア論理を直接的に使いたい、という理由があります。つうわけで、ホーア論理をTTPLを使って説明します。ただし、最初に言っておきますが、僕は（ホーア論理のような）プログラム証明を推奨する気はありません（どっちかいうと反対派）。それでも、理屈は知っておかないと、それから先に進めないってことはあります。内容： ホーア式 ホーア式の正しさ プログラムの証明 こんなにめんどくさい なにが重要か ●ホーア式ホーア論理の式（ホーア式とか、ホーア・トリプルと呼ばれる）は…

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

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

…契約に限らず、一般のホーア式もプログラムコードに翻訳する方法を考えてみました。特に、全称限量子（「すべての…に関して…」を意味する）の扱いを工夫してみます。（これは、「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)によると、トニー・ホー…

…] T2の制約部分（ホーア制約式の集まり）は、T1の制約部分を拡張している。 このとき、「T2はT1のサブタイプである（T1はT2のスーパータイプである）」と言ってかまいません。型階層を図に描くとき、普通はスーパータイプを上のほうに描くので、T1は上位、T2は下位だと言ってもいいでしょう。下層にいくほど実装は大変になるこの世で一番簡単な仕様（型と同義語）は次です。 spec Any { interface { } /* 制約はない */ } インターフェースは空っぽで、制約式…

…論理式として書く。 ホーア制約 ： “事前条件、実行文、事後条件”の3つ組。もし事前条件が満たされていれば、実行後に事後条件も満たされることを要請する。事前条件、事後条件は論理式、実行文はメソッド呼び出しの列。 ホーア制約は、（オリジナルの記法とは波括弧の使い方が逆だけど）「(事前条件){実行文}(事後条件)」という形にします。まずは不変制約を一発： 制約1 (-1 この制約（条件）により、a()の値が-10になったり300になるような実装は即刻排除できます。（&&を使わずに…

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

…/β}qに対する命題ホーア論理のような推論規則が必要だ。次は必要だろう（ないと辛い）。 |- p{/}p p{α/β}q, q{η/ξ}r |- p{α;η/β;ξ}r p'⇒p , p{α/β}q |- p'{α/β}q q⇒q' , p{α/β}q |- p{α/β}q' α、βなどは列言語と考えて、それなりの規則も要るだろう。たとえば： p{α/β}q, p{η/ξ}q |- p{(α|η)/(β|ξ)}q で、とりあえず、transducerやオートマトンの議論は、イ…

… + 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以上の状態…

…明／条件式（たとえばホーア論理式で書かれた制約）だとして、実装Mに対して、「M satisfies α」という言明（メタ表明、judgement）にハッキリした意味を持たせない限り、仕様の議論は何もできません。「M satisfies α」は論理（モデル論）における「M |= α」とまったく同じこと（だと定義できます）。まー、実際には、仕様（制約）が1個の論理式で書けるとは限らないので、A = {α1, α2, ...}を論理式の集合（これが仕様記述に対応する）として、「M …