Kの紹介と検証器の話

adventk.asc

Semantic-Based Program Verifiers for All Languages

Table of Contents

• 前置き
• 文献情報
• 前提知識
  • 𝕂 flamework
  • プログラム検証
• 具体例
• Matching Logic Reachability
• Matching Logic
  • Reachability Logic
  • ホーア論理との比較
• 実装と評価
• 後書き

前置き

このgistは今年読んだ一番好きな論文2017 Advent Calendarの1日目の記事です。

去年、覚え書きのような記事で参戦したら、歓迎の言葉に加えて参加賞まで貰ってしまった者です。あれで終わらせるのは申し訳ない以前に悔しいので、今回はよそゆきの文章でガッツリ書いてリベンジすることで感謝の言葉に替えたいと思います。

読者としてはプログラミング言語（C言語が望ましい）に触ったことがある人を想定しています。特に「コンパイル」「型」「ポインタ」といった概念を知っていれば序盤は理解しやすいでしょう。特にポインタという用語は記事中でも割と使っています。

内容的にはプログラム検証の話なので、述語論理くらいまで知っているとだいたい通じるような記事にするのが目標です。
どちらかというと背景部分の説明重視で、色々端折ったりしていますが、それ以上に踏み込んだ話^[1]が気になる人は元論文読んだ方が手っ取り早いと思います^[2]。
それでもそれなりの長さなので、まあ適当に読み飛ばしてください。

どちらかというと趣味で読んだ論文で、自分の研究分野とは近からず遠からずという感じなので、不正確な内容を含むかもしれませんがご了承ください。

文献情報

タイトル

Semantics-Based Program Verifiers for All Languages

著者

• Andrei Stefanescu

• Daejun Park

• Shijiao Yuwen

• Yilong Li

• Grigore Rosu

出典

OOPSLA 2016

去年発表のもので申し訳ないですが、11月開催なのでほぼ今年みたいなものでしょう。もちろん読んだのは今年です。

OOPSLAは プログラミング言語学会四天王^[3]なんて呼ばれたことがあるようなトップカンファレンス^[4]なので、十分に期待できるものだと思っていいでしょう。

ざっくりした内容としては「複数言語対応の共通検証基盤を作って実験しました」といったところでしょうか。複数言語に対応可能というところがミソです。

前提知識

まずは説明を盛りつつ、背景の話をします。前提知識といいつつ、僕としてはここだけでも覚えて帰ってもらえれば割と満足ではあるのですが……。

今回は K で書かれた言語の 検証器 を生成する話なので、この2点について説明します。

𝕂 flamework

筆者らの研究室で作っているK frameworkというプログラミング言語作成ツールがあります。公式の言葉を借りれば「rewrite-based executable semantic framework」とのこと。
ひどい名前に反して実はけっこう凄いツールであることを、プログラム言語のつくりと共に説明しましょう。

プログラミング言語は、形を表す シンタックス（文法） と動作を表す セマンティクス（意味論） からできています。例えば、「 if(b) B1 else B2 はbが数値、B1とB2がブロックで、全体として文を表す」というのがシンタックスで、「 if(b) B1 else B2 はbが0でないときはB1、それ以外はB2と同じ意味である」というのがセマンティクスです。
一般に、シンタックスはyaccやPEGといったツールによって記述されます。広く使われる形式であるため一度定められて仕舞えば再利用もし易く、比較的扱い易いと言っていいでしょう。一方、セマンティクスは普通、自然言語やプログラムによって記述されます。要するに数十〜数百ページに及ぶ仕様書や、コンパイラ・インタプリタといった処理系が先ずあって、形式的な意味論というのは必要になった時に既存のものに合わせて作るようなことが多いわけです。

Kは、セマンティクスもツールを使って書くようにしましょう、というものだと思ってください。さらにシンタックスも書くことができます。
シンタックスとセマンティクスが揃えば言語定義はもうできたと言っていいので、あとは自動で処理系やらデバッガやら諸々のツールを生成してくれる、というのがKのコンセプトです。筆者らの研究室のウェブサイトでは、このコンセプトの表現に以下のような図を用いています。

Kはまだまだ発展途上なので、この図の中で現在できているのはシンボリック実行、パーサ、デバッガ、くらいに見えます^[5]。
この論文では、プログラム検証器を作ってこの図の穴をまたひとつ埋めたことになりますね^[6]。

ここで重要なのは、全て同じひとつの言語定義から生成される点です。
パーサもデバッガも一度に生成できて楽というのももちろん重要ですが、それらが全て同じ定義を共有していることに注目してください。つまり、それぞれのツールが異なるバージョンの文法を参照しているとか、セマンティクスの定義が微妙にずれているとかいうことがないため、ツールの信頼性が高くなると考えていいでしょう。
これは特に検証器などにとっては重要な性質です。

Kの開発チームは言語定義作成をかなり頑張っていて、githubを見ると20近い既存言語についてリポジトリがあります^[7]。
つまり、Kにツール生成機能を追加する度に、20言語においてツールが利用可能になる……と言ってしまうと少し過言かもしれませんが、まあだいたいそういうことです。

ちなみに、Kにおいては、シンタックスはBNF的に、セマンティクスは操作的意味論の一種を使って書きます。

プログラム検証

プログラム検証 とは、プログラムを検証することです。形式検証とか呼ぶこともあるようです。
一般にプログラムの動作を保証したい時には、実際に入力を流し込んで期待する出力が得られるか確認するテストが主に用いられます。これは多数の入出力例を用意する必要があり、また普通は実際にプログラムを動かさなければ検査できません。
一方でプログラム検証は、入力が無限であっても漏れなく確認でき、また実行することなく検証可能であることが強みです。まあその分手法として重かったりはしますが。

具体的にどういうことを検証したいかというと、例えば「データの入ってないところから無理にデータを取り出そうとしていない^[8]」や「この関数の引数に長さが2以上の整数配列を渡したとき、その返り値は配列のどの要素よりも大きい」みたいなものを想像してください。もっと具体的な例はあとで出てきます。

さて、世の中にプログラム検証器は既に色々ありまして、例えばC言語ならVCCとかFrama-CとかVerifastとか……まあ色々あります。
で、これらのツールは、基本的に中間言語を使います。つまり、プログラムを検証し易い言語に変換し、検証したいことを同じく分かり易いように変換して、汎用的な検証器に投げるというわけです。

しかし筆者らは、中間言語への翻訳そのものが難しいものであり、バグを生むだろうと主張します。論文中では実際に検証器VCCの偽陽性があることなどを指摘し、これは中間言語への変換が正しくないためであると述べています。
プログラミング言語のセマンティクスを（ほぼ）そのまま流用できるような論理体系を構築し、その中で検証したい条件を書くことができれば、そんな間違いは起こらないはず……というのが、この論文のもう一つの（そして論文で主に語られている）目的のようです。

具体例

この研究の目標として、「こういうものをこんな感じで示したい」という例を示します。

まず、二分木構造nodeと、そこに値を挿入する関数insertを定義したプログラム片があります。ポインタを扱っているあたりが挑戦的ですね。

struct node{
  int value;
  struct node *let, *right;
}

struct node* new_node(int v){
  struct node *node;
  node = (struct node *)malloc(sizeof(struct node));
  node->value = v;
  node->left = NULL;
  node->right = NULL;
  return node;
}

struct node* insert(int v, struct node *t){
  if(t == NULL) return new_node(v);
  if(v < t->value) t->left = insert(v,t->left);
  else if(v > t->value) t->right = insert(v,t->right);
  return t;
}

このinsertは、二分探索木（BST）が引数だった場合、返り値がBSTになるように作られています。例えば、次の図はinsertを[8,3,6,10,14,1,13,7,4]の順で行った時にできるBSTです。

となれば当然、insertが本当にそういう風にできているのか検証したくなるわけですね。なりますよね？
このツールでは、以下のように書くことができます。

rule
  <functions>FUNCTIONS:Map</functions>
  <structs>STRUCTS:Map</structs>
  <mem>...MEM:Map(tree(L1, T1:Tree) ⇒∀ tree(?L2, ?T2:Tree))...</mem>
  <threads>
    <thread>...<k>
      insert(tv(V:Int, int), tv(L1:Loc, struct node))
        ⇒∀ tv(?L2:Loc, struct node)...
    </k>...</thread>
  </therads>
requires bst(T1) ∧ -2147483648 ≦ V ∧ V ≦ 2147483648
ensures bst(?T2) ∧ tree_keys(?T2) = {V}∪tree_keys(T1)

いきなりXMLが出てきて面食らったかもしれません。これはプログラムと状態をまとめて扱うためにKで使われている表現方法です。 <k>〜</k> がプログラムを表していることがわかれば、ざっくり次のように読めます。
「requireの条件（bst(T1)〜）を満たしているとき、矢印の右側（tree(L1,T1:Tree)、insert(〜)）は必ず矢印の左側（tree(?L2,?T2:Tree)、tv(〜)）に置き換わり、ensuresの条件（bst(?T2)〜）を満たす」
これは端的にいえば、BSTであるL1に対してinsert(L1,V)を行った時、L1にVを加えたBSTになるというだけです。214783648はint型で表現できる範囲を表しています。?Xは「その条件を満たすようなXが存在する」くらいの意味です。

実際にはここでbstやtv, tree_keysの定義も書かねばならないはずですし、それを抜きにしてもこの程度のことを検証するには書く量が多く感じられるかもしれません。
これに関しては、筆者らは「もっと簡単な記述から変換することが可能だよ」と言っています。一般的な述語の定義もセットにすれば、記述量は十分少なくなるでしょう^[9]。

論文ではさらにJavaとJavaScriptで同様のことを書いているのですが、ここでは省略します。少しだけ言及すると、それぞれの仕様（満たして欲しい条件）の記述は、少なくともbstの定義などに立ち入らない範囲では割と似ています。

Matching Logic Reachability

ここから技術的詳細に入っていきます。述語論理のわからない人は、このまま『実装と評価』まで読み飛ばしてしまった方がいいかもしれません。

Matching Logic

Matching Logicは、この論文のlast author（Kプロジェクトのボスでもある）が考案した論理体系です。論理式が型（sort）を持つこと、論理式に真理値ではなく集合が割り当てられることが特徴になるでしょうか。

Matching Logicの論理式は、プログラム実行中の一時点を切り取った時のシステムの状態を表すものです。状態Xが性質Pを満たす時、Pを表す論理式φに割り当てられる集合にXに対応する値が含まれる……などと言葉で説明すると余計混乱しそうなので、定義を見ていきましょう。
型の集合Sと記号の集合Σ、S∋s型の変数の集合Var_sがあったとき、matching logicのs型の論理式φ_sは、以下の要素から構成されます。さっきの仕様と書き方が若干違いますが、一旦忘れてください。

• x：変数（ただしx∈Var_s）

• σ(φ_s1, φ_s2, …​ , φ_sn)：定数（ただしσ∈Σ）

• ¬φ_s：否定

• φ_s ∧ φ_s：論理積

• ∃x.φ_s：存在量化（ただしx∈Var_s）

これだけではただの文字列のようなもので、記号に大した意味はありません。例えばplus(1,2)という式を3にすることはできません^[10]。

「全称量化は？」と思った方もおられるかもしれませんが、論理式の中には出てきません。後で説明しますが、自由変数が一番外側で似たようなことになります。
「論理和は？」と思った方もおられるかもしれませんが、構文としては出てきません。論理和の働きをする記号は作れるので、それで十分ということかと思います。

この論理式は パターン とも呼ばれ、∃x.mult(x,2)であれば4とか-18とかに "マッチ" することが期待されます。そのようにモデルを作り、論理式からモデル中の値への変換関数ρ’を作ります。
各変数にモデル中の値を割り当てる関数ρがあった時、ρ’はρから作られる関数で、パターン中の自由変数の値がρによって定められる時にパターン全体がとり得る値の集合を返します。
定義を書くのは面倒なので、一つ例を見てなんとなく納得してもらいます。納得できなければ原文を当たってください。
以下、xを3、yを2に割り当てるようなρから得られるρ’を[x:3,y:2]で表すものとし、σ∈Σの変換先はいい感じに与えられたとします^[11]。この時、パターン ∃y.(plus(x,y) ∧ is_even(y)) を、自然数の集合へ変換してみましょう。

[x:3,y:2](∃y.(plus(x,y) ∧ is_even(y)))
= [x:3,y:0](plus(x,y) ∧ is_even(y)) ∪ [x:3,y:1](plus(x,y) ∧ is_even(y)) ∪ …
= ([x:3,y:0](plus(x,y)) ∩ [x:3,y:0](equal(is_even(y),true))) ∪ ([x:3,y:1]plus(x,y) ∩ [x:3,y:1](equal(is_even(y),true))) ∪ …
= ([x:3,y:0](x) + [x:3,y:0](y) ∩ Is_even([x:3,y:0](y)) = [x:3,y:0](true)) ∪ ([x:3,y:1](x) + [x:3,y:1](y) ∩ Is_even([x:3,y:1](y)) = [x:3,y:1](true)) ∪ …
= ({3} + {0} ∩ Is_even({0}) == True) ∪ ({3} + {1} ∩ Is_even({1}) == True) ∪ …
= ({3} ∩ N) ∪ ({4} ∩ φ) ∪ …
= {3, 5, 7, 9, 11, …}

gistは数式が綺麗に書けないのでしんどいですね。
途中で集合同士の加算のようなことをしていますが、ここで全ての関数は集合に対して拡張されており、例えば{1,3} + {2,7} = {3,5,8,10}です。

結局のところ、 ∃y.(plus(x,y) ∧ is_even(y)) というパターンは（ρで定められる）x以上の数に1つおきにマッチします。
このように、割り当てρにおいて値γがパターンφにマッチするとき、 (γ,ρ)⊨φ と書きます。今の例であれば、 (5,[x:3]) ⊨ ∃y.(plus(x,y) ∧ is_even(y)) といった具合です。

一つ重要な点として、Matching Logicは、Separation Logic(分離論理)という論理体系を模倣できます。分離論理はポインタやメモリについて扱いたい場合に用いられるものであるため、その手の証明テクニックやらがそのまま使えるMatching Logicも実用的なものだ、ということです。

Reachability Logic

論理式はシステムの状態を表すものでしたが、検証のためにはその変遷を追う必要があります。そのために、⇒^∃と⇒^∀という2つの矢印（ ルール ）を使います。前者が主にセマンティクスを、後者が仕様を記述するためのものです。それぞれ「one-path reachability」「all-path reachability」と呼びます。

まず、 セマンティクスとしての one-path reachabilityを見てみましょう。（Kで採用しているような）操作的意味論では、例えば if(b) B1 else B2 ⇒ B1 when b≠0 のように規則を書きます。ここで when b≠0 の部分は右辺ではなく、このルールが適用されるための条件だと思ってください。これをone-path reachabilityに直すと、 if(b) B1 else B2 ∧ b≠0 ⇒∃ B1 となります。
φ⇒^∃φ’は、(γ,ρ)⊨φであるような任意のγとρに対して、(γ',ρ)⊨φ’となるようなγ’が存在することを意味します^[12]。 例で言えば、B1とB2の中身がなんであれ、この形にさえなっていればB1に書き換えることができる、ということですね。 こうして言語のセマンティクスから機械的な変換によって得られたルールの集合を、reachability systemと呼びます。以降、Sと書いたら任意のreachability systemを表すとします。

次に、仕様の表し方を定義していきましょう。(γ,ρ)⊨φである任意のγとφに対して、Sのルールを繋げていくことで、(γ',ρ)⊨φ’であるようなφ’に辿り着けるルートが存在するか無限列を作ることができる場合、 仕様としての one-path reachability φ⇒^∃φ’が成り立つとします。直観的には、Sのルールを一つ繋げるということは計算を1ステップ進めることなので、φを満たす状態から実行した時にφ’を満たす状態に辿り着くor無限ループに陥る可能性がある場合にφ⇒^∃φ’であるといえます。「辿り着く 可能性がある 」という言い方をしているのは、一般にSは非決定的な場合があるからです。プログラミング言語の仕様をよく見ると「評価順序は処理系依存」などの記述があることは少なくありません。
同様に、(γ,ρ)⊨φである任意のγとφに対して、φから初めてこれ以上ルールを適用できないところまでSのルールを繋げていったとき、必ずその中のどこかで(γ',ρ)⊨φ’であるようなφ’が出現するとき、all-path reachability φ⇒^∀φ’が成り立つとします。つまり、φを満たす状態から実行していった時に、停止するなら 必ず どこかでφ’を満たす状態を通っている、ということです。
任意の状態に対してS中に適用できるルールシステムが一つしかない、つまりシステムが決定的に働くとき、φ⇒^∃φ’とφ⇒^∀φ’は一致します。

この2つのreachabilityがあれば割と実用的なことが表せそうな気がします。具体的にどれくらい実用的かというと、この分野でよく使われるホーアの三つ組をさらに一般化したもの^[13]なので、十分実用的だと言えるでしょう。

ここまでくれば、具体例として示したCプログラムに対する仕様を読むことができます。仕様は以下のようなものでした。

rule
（前略）
insert(tv(V:Int, int), tv(L1:Loc, struct node))
  ⇒∀ tv(?L2:Loc, struct node)
（後略）

requires bst(T1) ∧ -2147483648 ≦ V ∧ V ≦ 2147483648
ensures bst(?T2) ∧ tree_keys(?T2) = {V}∪tree_keys(T1)

上で説明した記法に置き換えると、次のような感じになります。

（前略）insert(tv(V, int), tv(L1, struct node))（後略）
  ∧ bst(T1) = true ∧ (-2147483648 ≦ V) = true ∧ (V ≦ 2147483648) = true

⇒∀

∃L2. ∃T2.
  （前略）tv(L2, struct node)（後略）
  ∧ (bst(T2)) = true ∧ (tree_keys(T2) = {V}∪tree_keys(T1)) = true

上の条件を満たすような状態において、自由変数（例えばV）の値が何であろうと、どんな遷移をしようと、必ず insert(tv(V, int), tv(L1, struct node)) の値^[14]は ∃L2.tv(L2, struct node) の値と等しくなる、という感じですね。

さて、張り切って書いたら一万文字を超えてしまいました。一番面白い部分も終わったことですし、駆け足でいきましょう。この後にreachabilityを導くための推論システムについて書かれているのですが、ここでは触れません。気になる人は論文の図4を参照してください^[15]。このシステムは健全であり、かつ巧いモデルを与えてやれば完全（relatively complete）なので、妥当なものであると考えてよいでしょう。
こうして得られる論理体系をReachability Logicと呼びます。

ホーア論理との比較

プログラムの検証をする際に広く使われるホーア論理と、今回導入したReachability Logicを比較していきます。論文では実例を交えて色々と解説していますが、要点をまとめると以下のような感じ。最後の項目は個人的な感想です。

• プログラムを変形しないとホーア論理が使えないような場合でも、Reachability Logicなら変形することなく使える

• ホーア論理ではプログラミング言語に合わせて推論規則を作る必要があるが、Reachability Logicは固定

• セマンティクスをそのまま使えるので、変換の手間がかからない

• 証明のサイズ（長さ）はReachability Logicの方が大きくなった

• 仕様の記述量も本質的には大差なさそう^[16]

実装と評価

冒頭で述べた通り、この理論を用いた検証器生成器がKに実装されています。2.5人年^[17]かけて頑張ったそうです。
実装の工夫については個人的にあまり興味が無いのですが、 SMTソルバZ3を用いている点だけ触れておきましょう。SMTソルバとは特定の形式で与えられた問題を自動で解く汎用の問題解決ソフトだと思ってください。Kでは証明全体をSMTに落とし込んで解かせる訳ではなく、一部の推論規則の中で部分的にSMTソルバを呼び出すような形をとっているようです。

評価としては、連結リストおよび木に対する18の基本的操作について、その性質を検証して時間を計測しています。対象言語はC, Java, JavaScriptに加え、仕様が単純なKernelCという言語の4つ。
結果を見ると、言語仕様/プログラムの複雑度が増すにつれ検証時間が（順当に）長くなっていきます。JavaScriptを例にとると、検証にかかる時間は1秒未満から1分程度。検証内容がより複雑になればもちろん更に時間がかかるでしょうが、それでも十分な結果に見えます。最も複雑なC言語だと3秒から5分となります。まずまずの結果ではないでしょうか。
筆者らはこの結果から、本システムは十分に実用的であると結論しています。

続いて、Kにおける各言語のセマンティクスおよび仕様の記述コストについて。表でまとめます。

	C	Java	JavaScript
セマンティクス開発期間（ヶ月）	40	20	4
セマンティクスルール数	2,572	1,587	1,378
セマンティクス行数	17,791	13,417	6,821
セマンティクス修正期間（日）	7	4	5
セマンティクス修正ルール数	63	38	12
セマンティクス修正行数	468	95	49
仕様数	36	31	31
定義数	27	27	27

各言語のセマンティクスは今回の研究とは無関係に開発されたものですので、こちらに要した手間はあまり気にしないことにしましょう。
今回使うにあたってバグに気付いたとか検証しにくかったとかで変更を加えており、それが『セマンティクス修正』の項です。仕様数は読んで字の如く。定義数というのは、上であげたbstなどの定義をいくつ書いたかを意味します。
Kに対象言語のセマンティクスが存在するという前提下においては、1週間もあれば検証器が作れてしまうわけです。「言語非依存の検証基盤を作る」という目的は十分に達成できたのではないでしょうか。望む言語のセマンティクスがあるかどうかは……開発チームに期待しましょう。Kが言語開発のスタンダードになれば、そういう心配もせずに済むのでしょうが、そんな未来は暫く訪れそうにないですね。

最後に、章題からは外れますが、future workとして挙げられているものを見て終わりたいと思います。

• K自体を証明アシスタントCoqで検証する（進行中）

  • これができれば、検証を間違う原因として残るのはセマンティクス（とZ3？）のバグのみ

  • 今回の証明システムは既にCoqで形式化されている（！？）

• データ構造に関する検証システム（進行中）

  • 詳細はわからないが、特化したシステムを作るということか

• 検証対象のソースファイル中に仕様を簡潔に書けるようにする

• タイムアウト等により自動で検証できなかった部分をCoqを使って手動証明できるようにする

• マルチスレッドプログラムへの対応

理論的な発展というよりは、ツールとして使い易く、世間のプログラムに適用できるように、という方向性でしょうか。数年後には、OSSを検証してみた論文なんかが出てくるかもしれませんね。

後書き

次のことについて見てきました。

• Kというなんだか面白いプログラミング言語開発ツール

• セマンティクスとプログラム仕様を同じところに落とし込むReachability Logic

• それらを利用した言語非依存の検証基盤の実用性

個人的に、3つのアイデアはそれぞれ非常に興味深く、「今年読んだ一番面白い論文」に相応しいと思っています^[18]。読みながら書いていたからというのもありますが、ちょっとテンションが上がって思ったよりも長文になってしまいました。ここまでお付き合いいただきありがとうございました。
今年読んだ一番好きな論文2017 Advent Calendarは現時点でまだ募集中のようです。というか明日から1週間以上、誰も登録していなくて寂しいです。これを読んでいる皆さんの論文紹介に明日以降出会えることを楽しみにしています^[19]。

お粗末様でした。

---

1. 特にこの記事ではかなりインフォーマルな書き方をしているので、定義の詳細などは論文の方を見ればだいたいちゃんと載っています。

2. もちろん聞いてもらえればわかる範囲でお答えします。

3. 4つともACM（情報系最大手学会） SIGPLAN（プログラミング言語系分科会）のpremier forum/conferenceです。ざっくりPOPL:理論、PLDI:実装、ICFP:関数型、SPLASH/OOPSLA:応用という認識。

4. 「トップカンファレンス」という概念ってもしかして情報系以外にはあまり通じなかったりするのでしょうか。

5. 逆に、ドキュメント生成など、ここに載っていないツールも存在するようです。

6. ただ、 チェンジログを見ると、2014年の時点で既に検証器は存在したようです。これと今回のものが同じものなのかは調べていませんが、漸く使えるレベルになったから発表した、とみるべきでしょうか。

7. 作りかけのものもあるかもしれませんが、逆に開発チーム以外が作った（この一覧に載っていない）ものもなくはないので、差し引き0と判断しましょう。

8. これに違反する場合は変数が未定義であるとか、ポインタの値がおかしいとかですね。特にC初心者なら一度は苦しめられたのではないでしょうか。

9. しかし、この変換も（他の検証器における変換よりはよっぽど簡単そうではあれど）バグの温床になり得るように思えるのですが大丈夫なのでしょうか……。

10. まあ公理として追加すればいいだけの話ではあるのですが、ややこしくなるので置いておきます。

11. 論文では、ダッシュではなくバーを使って書いていますし、リスト風の書き方も存在しませんが、面倒なのでここではこの記法を用いています。

12. 実際には、まずパターンの組φ⇒∃φ’として定義され、(γ,ρ)⊨φの時(γ',ρ)⊨φ’となるようなγ’が存在する場合にweakly well-definedとする……という手順があるのですが、混乱を避けるためここでは省略しました。

13. 空のプログラムはそれ以上何も起きないという前提下で、事前条件と実行するプログラムを矢印の左側に、事後条件と空のプログラムを矢印の右側にもってくれば一致するのだと思います。

14. 正確には「取りうる値の集合」です。定義によってはinsertがランダムな値を返すかもしれませんし、実際ポインタなので実行時まで決まらないでしょう。後ろも同様。

15. 本当に参照する人のために少しだけ補足しておくと、A, C, Qという記号が追加されていることに注意してください。AとCはルールの集合で、ループで余帰納法を用いるために使われます。最終的に示したいのはAもCも空の場合です。Q∈{∃, ∀}で、通常前提のものを受け継ぎますが、Stepで∀を、AxiomでSから∃を作りだすことができます。あとはフィーリングで。

16. とはいえ、仕様の書き方はセマンティクスの書き方から影響をモロに受けるので、書きやすさは落ちてるというべきかもしれません。その分、記述でできる内容の自由度は上がっているとは思いますが。

17. 「人月」はよく聞きますが、「人年」はあまり聞かない気がします。英語論文を読んでると「実装にX人年かかった」みたいな記述は時々見かけますが、日本語ではあのみずほ案件ですら「20万人月」と頑なに月を重んじています。やはり語呂でしょうか。

18. まあ、アドベントカレンダーに登録した時点ではアブストラクト程度しか読んでいなかったのですが、その時点で絶対に面白いという確信があったのでいいのです。

19. 院生でない方やクリスマスを過ぎてからこれを読んでいる方はすみません。