https://m-hiyama.hatenablog.com/entry/2026/03/02/163549

ホーアオートマトンは、“状態ソートを含む指標のモデル”となるものです。今言った「状態ソートを含む指標のモデル」は、ホーアオートマトンの手短〈てみじか〉な説明になっています。が、これだけでは通じないでしょう。通じないだけならいいのですが、言葉の印象から誤解されることもありそうです。

言葉の印象からの誤解は、僕の長年の悩みです -- 永遠に解決できそうにないですけどね。分野・コミュニティ・人・場合により、言葉や習慣が違うのですよね。その食い違いが、コミュニケーションを困難にします。同じ言葉・習慣に基づいたコミュニケーションでも、同義語や曖昧多義語によりコミュニケーション上の齟齬が発生することもあります。

ホーア論理とホーアオートマトンを語る際に、予想される言葉と習慣に関わる問題点を先に指摘しておくことにします。特に、ホーア論理とホーアオートマトンでは肝となる概念「指標」が、言葉・習慣の問題からなかなかうまく伝わらないので、指標に関しては詳しい説明をします。言葉の問題の指摘だけでなくて、概念そのものをGo言語による具体例と共に説明します。

記事内で使う文字の色の約束は、「ホーア論理とホーアオートマトン 1/n // 文字の色の約束」を確認してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
%\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\parto}{\supset\!\to}
\newcommand{\tto}{ \mathrel{!\!\!\to} }
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\HoareAutom}{\mathbf{HoareAutom}}
\newcommand{\SimpleHoareAutom}{ \mathbf{SimpleHoareAutom} }
`$

内容：

シリーズ・ハブ記事

ホーア論理とホーアオートマトン 1/n

指標、シグニチャ、プロファイル、インターフェイス

僕は「関数」と「写像」を区別しません。人により場合により区別することもあるでしょうが、僕は「関数」と「写像」は同義語扱いです。同義語を山形括弧に入れて示すことがあります（これは僕個人の習慣です）。関数と写像は区別しないので、「関数〈写像〉」とか「写像〈関数〉」という表記を使うことになります。日本語でも英語でも意味は変わりませんから、「関数〈function | 写像 | map |mapping〉」のように、何個も同義語を並べることもあります。

指標〈signature | シグニチャ〉は、仕様記述で最も基本的で最も重要な概念です。が、「シグニチャ」という言葉は、関数・メソッドの引数の仕様という意味で使われるので、それを連想する人も多いでしょう（そして、誤解・誤認がはじまる）。「関数・メソッドのシグニチャ〈signature of function/method〉」と言った場合、おおよそ次のような意味があるようです。

関数・メソッドの名前と引数達の仕様のこと、場合により戻り値の仕様も含まれる。

シグニチャの厳密な定義は、プログラミング言語ごとに違います。C言語では、「シグニチャ」という言葉を使わずに「関数プロトタイプ〈function prototype〉」と呼びます。

僕は、関数プロトタイプの意味でシグニチャ〈指標〉を使うことはありません。「シグニチャ」に（ほぼ）相当する言葉としては「プロファイル」を使います。圏論の文脈で、射の域と余域を示す $`A \to B`$ で示される情報がプロファイル〈profile〉です。プロファイルは、圏の対象の順序対〈oerdered pair〉です。プロファイル（対象の順序対）によりホムセット〈homset〉が特定されます。

圏 $`\cat{C}`$ の射 $`f`$ のプロファイルが $`A \to B`$ であることは、

$`\quad f:A \to B \In \cat{C}`$

と書きますが、これはホムセットへの所属関係 $`f\in \cat{C}(A, B)`$ と同じことです。

仕様記述の形式である指標〈signature | シグニチャ〉に相当する概念は、多くのプログラミング言語に在ります。が、その呼び名はバラバラで、それぞれが微妙に違います。指標に相当する概念の（おそらく）一番ポピュラーな呼び名は「インターフェイス〈interface〉」でしょう。他の呼び名として、「プロトコル〈protocol〉」「型クラス〈type class〉」「コンセプト〈concepts〉」「トレイト〈trait〉」などがあります。類似はしてますが、同じというわけではありません。例えば型クラスは、“いわゆるインターフェイス”に加えて、オーバーロード解決のメカニズムを持っていたりします。

曖昧多義語、同義語・類義語

曖昧多義語の問題を少しでも解消するために、過去記事「同義語・多義語にホトホト困っている」で提案した方法は、アットマークにより分野や文脈を明示することです。過去記事では次の例を挙げています。

フィールド＠物理（電磁場などの「場」）
フィールド＠代数（加減乗除ができる代数系）
フィールド＠データベース（レコードの成分）

これで「フィールド」の異なる意味を区別できます。曖昧多義語の意味解決がアットマークにより（多少は）できます。

一方で、“フィールド＠データベース”（データベース分野で使われる用語「フィールド」）に同義、あるいは類義の言葉は色々あります。ナニカを並べたり配置したりした複合データにおける“ナニカ”をなんと呼ぶか？というと：

成分〈component〉
要素〈element〉
項目〈item〉
メンバー〈member〉
エントリー〈entry〉
フィールド〈field〉
属性〈attribute〉
カラム〈column〉
プロパティ〈property〉
スロット〈slot〉

などがあります。これらは異綴同義語〈いてつどうぎご〉、あるいは異綴類義語〈いてつるいぎご〉です。

僕の感覚だと、「フィールド」「属性」「カラム」は完全に同義だと思ってますが、これらの言葉の背後には、意味だけではなくて派閥(?)が在ったりします。うかつに「同じでしょ」とか言うと石が飛んでくるかも知れません。しちめんどくさい話ですわ。

過去記事「同義語・多義語にホトホト困っている」では、2つの語が同義であることを「≡」、類義であることを「～」で表すことにしています。前節の最初に言ったことは、“関数＠檜山” ≡ “写像＠檜山” と書けます。「＠檜山」を付けているのは、僕〈檜山〉の用法であり、一般的に関数 ≡ 写像（「関数」と「写像」は同義）とまでは言い切れないからです*1。

前節の言明「僕は、関数プロトタイプの意味でシグニチャ〈指標〉を使うことはありません」は、次のように書けます。

　　シグニチャ＠檜山 ≢ 関数プロトタイプ＠C言語

「≢」は、「≡」の否定*2で、同義ではないことです。“関数プロトタイプ＠C言語” 類似の概念を僕は“プロファイル”と呼んでいて、それはJavaのシグニチャと類似です。これは次のように書けます。

　　関数プロトタイプ＠C言語～プロファイル＠檜山～シグニチャ＠Java

“指標＠檜山”と類似の概念が各種のプログラミング言語に在る話は、例えば次のように書けるでしょう。

　　指標＠檜山～インターフェイス＠TypeScript ～プロトコル＠Swift ～型クラス＠Haskell ～コンセプト＠C++ ～トレイト＠Rust

「同義語・多義語にホトホト困っている」以外にも、同義語・多義語の問題や対策を述べている過去記事があります。

用語のバリエーション記述のための正規表現
曖昧さを減少させるために、式にフォーマット指定（形式的表現や半形式的表現における曖昧性の話）
モノの種別とモノの相対役割り
同義語・多義語の問題：タグによる修飾と分類
曖昧性を減らす： Diag構成を事例として
デジタル語彙目録:: 名前の管理

常にアットマーク（'＠'）や同義性（'≡'）、類犠牲（'～'）を使うのは煩雑過ぎますが、勘違いが起きそうな場面では、これらの記法を使うことがあります*3。

なお、10年前（2016年）の記事でも、言葉と習慣（つまり文化）のギャップがあって「なかなか伝わらない」という愚痴を書いてましたね。

一般化されたマイヒル／ネロードの定理 2：文化的なギャップを乗り越えるための対訳表

指標

ここでは、圏論を背景とした指標〈signature〉の概念を紹介します。指標は、圏のなかで定義される構造を表現する記号的形式です。以下は、可換半群〈commutative semigroup〉を定義する指標です。

$`\T{signature }\T{CommSemigroup}\In \mbf{Set} \:\{\\
\quad \T{sort }U\\
\quad \T{operation }\mrm{op} : U\times U \to U\\
%
\:\\
\quad \T{// 法則1: 結合法則}\\
\quad \T{equation }\mrm{assoc} ::\\
\quad \T{For }x, y, z : U\\
\qquad \mrm{op}(\mrm{op}(x, y), z) = \mrm{op}(x, \mrm{op}(y, z) )\\
%
\:\\
\quad \T{// 法則2: 交換法則}\\
\quad \T{equation }\mrm{comm} ::\\
\quad \T{For }x, y : U\\
\qquad \mrm{op}(x, y) = \mrm{op}(y, x)\\
\}
`$

指標の文脈では、伝統的に「ソート〈sort〉」「オペレーション〈operation〉」という言葉が使われますが、より馴染みの言葉に言い換えれば：

　　ソート＠指標 ≡ 型＠お馴染み
　　オペレーション＠指標 ≡ 関数・メソッド＠お馴染み

ただし、集合圏のなか（$`\In \mbf{Set}`$）で考えているので、「型」は Sets-as-Types の立場で解釈します。つまり、ここでは「型 ≡ 集合」です。型に対する様々な立場については「集合論・圏論 vs. 型理論 // 型と型宇宙」を参照してください。

可換半群の場合は、法則が等式なので equation というキーワードを使ってますが、一般には法則〈law〉です。指標の法則についても同義語があります。

　　法則〈law〉 ≡ 公理〈axiom〉 ≡ 制約〈constraint〉 ≡ 条件〈condition〉

上の例の結合法則〈associative law〉と交換法則〈commutative law〉は、可換半群の公理ともいうし、可換半群（であること）の制約ともいうし、可換半群の条件ともいいます。

「指標」という言葉は、普遍代数〈universal algebra〉、抽象モデル理論〈abstract model theory〉、インスティチューション理論〈institution theory〉、形式セオリーの理論〈theory of formal theories〉などでは普通に使われていますが、人により若干定義が違います。

ソート〈型＠お馴染み〉宣言とオペレーション〈関数・メソッド＠お馴染み〉宣言の部分（法則は入れない）を指標と呼ぶ人がいます。稀に、ソート宣言も外してオペレーション宣言の部分だけを指標と呼ぶ人もいます。僕は、ソート宣言・オペレーション宣言・法則をすべて入れたものを指標と呼んでいます*4。

法則を入れないで考えることはけっこうあります。法則を持たない指標は、無法則指標〈lawless signature〉と呼ぶことにしましょう。例えば、可換半群の指標から法則を単純に取り除くと、次の無法則指標になります。

$`\T{signature }\T{CommSemigroup}\In \mbf{Set} \:\{\\
\quad \T{sort }U\\
\quad \T{operation }\mrm{op} : U\times U \to U\\
\}
`$

ただし、法則がほんとにないなら可換半群とは呼べないので、適切に名前を変えるべきです。

$`\T{signature }\T{Magma}\In \mbf{Set} \:\{\\
\quad \T{sort }U\\
\quad \T{operation }\mrm{op} : U\times U \to U\\
\}
`$

「無法則〈lawless〉」という形容詞は、レンズに対して使っていることを2021年に知りました（無法則レンズ〈lawless lens〉）。以下の過去記事に書いています。

圏論的レンズ最初の一歩：ストリング図を中心に

形容詞「無法則」が便利なので、指標に対しても使うことにしたのです。以下の記事も参照してください。

有法則代数と無法則代数

オブジェクト指向風の指標

前節の指標の例は代数系〈代数構造〉を定義するものでした。この節では、オブジェクト指向風にデータ構造とメソッドを定義する例を挙げます。

オブジェクト指向風の指標では、状態空間を表すソート〈型 | 集合〉を特別扱いします。確かに特別扱いする必要はあるのですが、特別扱いの程度にバラつきがあり、分かりにくくなっています。ここではとりあえず、状態空間を表すソートも普通のソート〈型 | 集合〉として記述することにします。

指標を解釈する場は集合圏（集合と写像の圏）ではなくて、射が半決定性写像〈部分写像〉である圏 $`\mbf{SDet}`$ です（「ホーア論理とホーアオートマトン 2/n // 決定性、非決定性、半決定性」参照）。矢印「$`\to`$」は半決定性写像〈部分{関数 | 写像}〉です。矢印「$`\tto`$」は決定性写像だとします。法則はホーアトリプル〈Hoare triple〉の形で書きます。

$`\T{signature }\T{IntStack}\In \mbf{SDet} \:\{\\
\quad \T{sort }S\\
\quad \T{operation }\mrm{isEmpty} : S \tto \mbf{B}\\
\quad \T{operation }\mrm{top} : S \to \mbf{Z}\\
\quad \T{operation }\mrm{push} : S \times \mbf{Z} \tto S\\
\quad \T{operation }\mrm{pop} : S \to S\\
%
\:\\
\quad \T{// 法則1: スタックが空でなければ、top は動く}\\
\quad \T{law }\mrm{top} ::\\
\quad\T{For object }s : S \\
\qquad (\lnot s.\mrm{isEmpty}() )\{ s.\mrm{top}() \}( )\\
%
\:\\
\quad \T{// 法則2: スタックが空でなければ、pop は動く}\\
\quad \T{law }\mrm{pop} ::\\
\quad\T{For object }s : S \\
\qquad (\lnot s.\mrm{isEmpty}() )\{ s.\mrm{pop}() \}( )\\
%
\:\\
\quad \T{//法則3: push すると、スタックは空でなくなる}\\
\quad \T{law }\mrm{push} ::\\
\quad\T{For object }s : S,\: \T{value } v : \mbf{Z}\\
\qquad ()\{ s.\mrm{push}(v) \}( \lnot s.\mrm{isEmpty}() )\\
%
\:\\
\quad \T{// 法則4: push すると、push した値が top になる}\\
\quad \T{law }\mrm{push\_top} ::\\
\quad\T{For object }s : S,\: \T{value } v,w : \mbf{Z}\\
\qquad ()\{ s.\mrm{push}(v); w := s.\mrm{top}() \}( v = w)\\
%
\:\\
\quad \T{// 法則5: top の値を保存し、なにかを push してから pop すると、}\\
\quad \T{// 元の値が top になる}\\
\quad \T{law }\mrm{push\_pop} ::\\
\quad\T{For object }s : S, \T{value } v,w,x : \mbf{Z}\\
\qquad ( \lnot s.\mrm{isEmpty}() )\{
v := s.\mrm{top}(); s.\mrm{push}(x); s.\mrm{pop}(); w := s.\mrm{top}()
\}
( v = w)\\
\}
`$

これは、積む値が整数〈integer〉であるスタックの指標です。以下に詳しく説明しましょう。

$`S`$ はスタックの内部状態を表すソート〈型 | 集合〉です。$`\mrm{isEmtpy}`$, $`\mrm{top}`$, $`\mrm{push}`$, $`\mrm{pop}`$ はメソッドです。$`S`$ を特別扱いしてないので、メソッドは第一引数の型が $`S`$ である関数と考えます。

法則はホーアトリプルで書きますが、ホーアトリプル〈Hoare triple〉は $`P\{E\}Q`$ の形の式です。ここで、$`P, Q`$ は論理式、$`E`$ はプログラムの実行文です。論理式は丸括弧で囲んだ形にしています。$`()`$ は無条件、つまり、常に真であると評価されます。

ホーアトリプルの論理式と実行文には変数が含まれてもかまいません。ホーアトリプルの直前の $`\text{For}`$ で変数の宣言をします。$`\T{object }s : S`$ で宣言されたオブジェクト変数 $`s`$ は、実行中にメソッドにより変数の値（である状態）が変わるかも知れません。$`\T{value }v : \mbf{Z}`$ で宣言された変数は整数値（状態ではない値）を持ちます。$`v`$ などの変数の値は破壊的代入 $`:=`$ で上書きされます。

$`s.\mrm{isEmpty}()`$, $`s.\mrm{push}(v)`$ などは、$`\mrm{isEmpty}(s)`$, $`\mrm{push}(s, v)`$ の別表記に過ぎません。多くのプログラミング言語で採用されているのでお馴染みでしょう。

半決定性写像〈部分関数〉達の圏 $`\mbf{SDet}`$ で考えているので、論理式や実行文は未定義になるかも知れません。未定義とは、例外が発生したり無限ループに落ち込むことだと思ってください。

ホーアトリプルは、トリプル全体として一種の論理式です。次の条件をすべて満たしたときにホーアトリプル $`P\{E\}Q`$ は真だと評価されます。

論理式 $`P`$ が真だと評価される。（偽でも未定義でもない。）
実行文 $`E`$ の実行が正常終了する。（途中で例外が発生したり、無限ループに落ち込まない。）
論理式 $`Q`$ が真だと評価される。（偽でも未定義でもない。）

ホーアトリプルをテストコードだと考えると、「テストをパスした」といえる条件が上の3つの条件（のAND）です。

論理式としてのホーアトリプルに出現する変数は、暗黙に全称束縛されて〈universally quantified〉います。つまり、$`\T{For object }s:S,\T{value }v,w: \mbf{Z}`$ と宣言されていれば、ホーアトリプルは“すべての $`s, v, w`$ に対して”真であることが要求されます。特定の $`s, v, w`$ に対して真であるだけではダメです。

矢印「$`\tto`$」を使って、写像が決定性〈全域 | total〉であることを示すのは便利ですが、使わなくてもかまいません。次のような（ホーアトリプルによる）法則で決定性〈全域〉だと主張できます。

Go言語で書いてみる

前節の指標は、実在するプログラミング言語ではなくて、抽象的な構文で書きました。実在するプログラミング言語に翻訳してみましょう。Go言語への翻訳を試みてみます。

前節の指標を、無法則指標と法則の部分に分けます。無法則指標は次のようです。

法則部分を落とすわけじゃなくて、分けて書くだけなので、名前 $`\T{IntStack}`$ は変えません。この無法則指標（指標の一部）は、Go言語で次のように書けます。

package intstack

type IntStack interface {
  IsEmpty() bool
  Top() int
  Push(int)
  Pop()
}

パッケージ宣言があったり、メソッド名が大文字始まりだったりするのはGo言語の事情によります。また、Go言語では、状態の型 $`S`$ をインターフェイスに明示的には書きません。関数・メソッドが決定性であること（$`\tto`$）は、ホーアトリプルで書くことにします。

Go言語の習慣とメカニズムからは、法則の部分は別ファイルに書きます。比較しやすいように、ホーアトリプルによる法則（すぐ下）の後にGo言語のソースコードを示します。

$`
\quad \T{// 法則0A: isEmpty は常に動く}\\
\quad \T{law }\mrm{isEmpty\_total} ::\\
\quad\T{For object }s : S \\
\qquad ()\{ s.\mrm{isEmtpy}() \}( )\\
%
\:\\
\quad \T{// 法則0B: push は常に動く}\\
\quad \T{law }\mrm{push\_total} ::\\
\quad\T{For object }s : S,\: \T{value }v: Z \\
\qquad ()\{ s.\mrm{push}(v) \}( )\\
%
\:\\
\quad \T{// 法則1: スタックが空でなければ、top は動く}\\
\quad \T{law }\mrm{top} ::\\
\quad\T{For object }s : S \\
\qquad (\lnot s.\mrm{isEmpty}() )\{ s.\mrm{top}() \}( )\\
%
\:\\
\quad \T{// 法則2: スタックが空でなければ、pop は動く}\\
\quad \T{law }\mrm{pop} ::\\
\quad\T{For object }s : S \\
\qquad (\lnot s.\mrm{isEmpty}() )\{ s.\mrm{pop}() \}( )\\
%
\:\\
\quad \T{//法則3: push すると、スタックは空でなくなる}\\
\quad \T{law }\mrm{push} ::\\
\quad\T{For object }s : S,\: \T{value } v : \mbf{Z}\\
\qquad ()\{ s.\mrm{push}(v) \}( \lnot s.\mrm{isEmpty}() )\\
%
\:\\
\quad \T{// 法則4: push すると、push した値が top になる}\\
\quad \T{law }\mrm{push\_top} ::\\
\quad\T{For object }s : S,\: \T{value } v,w : \mbf{Z}\\
\qquad ()\{ s.\mrm{push}(v); w := s.\mrm{top}() \}( v = w)\\
%
\:\\
\quad \T{// 法則5: top の値を保存し、なにかを push してから pop すると、}\\
\quad \T{// 元の値が top になる}\\
\quad \T{law }\mrm{push\_pop} ::\\
\quad\T{For object }s : S, \T{value } v,w,x : \mbf{Z}\\
\qquad ( \lnot s.\mrm{isEmpty}() )\{
v := s.\mrm{top}(); s.\mrm{push}(x); s.\mrm{pop}(); w := s.\mrm{top}()
\}
( v = w)\\
\}
`$

package intstack

import "testing"

// 法則0A: isEmpty は常に動く
func Law0A_isEmpty_total(s IntStack) bool {
  s.IsEmpty()
  return true
}

// 法則0B: push は常に動く
func Law0B_push_total(s IntStack, v int) bool {
  s.Push(v)
  return true
}

// 法則1: スタックが空でなければ、top は動く
func Law1_top(s IntStack) bool {
  if !s.IsEmpty() {
    s.Top()
  }
  return true
}

// 法則2: スタックが空でなければ、pop は動く
func Law2_pop(s IntStack) bool {
  if !s.IsEmpty() {
    s.Pop()
  }
  return true
}

// 法則3: push すると、スタックは空でなくなる
func Law3_push(s IntStack, v int) bool {
  s.Push(v)
  return !s.IsEmpty()
}

// 法則4: push すると、push した値が top になる
func Law4_push_top(s IntStack, v int) bool {
  var w int
  s.Push(v)
  w = s.Top()
  return v == w
}

// 法則5: top の値を保存し、なにかを push してから pop すると、
// 元の値が top になる
func Law5_push_pop(s IntStack, x int) bool {
  var v, w int
  if !s.IsEmpty() {
    v = s.Top()
    s.Push(x)
    s.Pop()
    w = s.Top()
  }
  return v == w
}

抽象的形式でのホーアトリプルが、機械的にGo言語の関数に翻訳できているのが分かるでしょう。

法則とテストの違い

前節のGo言語ソースコード（2ファイル）は、指標 $`\mrm{IntStack}`$ を忠実に翻訳したものです。指標 $`\mrm{IntStack}`$ の情報は、実在する言語 Go に完全にエンコードされたと言えます。

ただし、前節のGo言語ソースコードは動くスタックを記述していません。整数を積むスタックのインターフェイスと満たすべき法則を書いているだけです。実際に動くスタックは、以下の雛形（の空っぽな部分）を埋めることで作られます*5。

type IntStackImpl struct {
}

func (s *IntStackImpl) IsEmpty() bool {
}

func (s *IntStackImpl) Top() int {
}

func (s *IntStackImpl) Push(v int) {
}

func (s *IntStackImpl) Pop() {
}

func NewIntStack() IntStack {
}

実際に動くスタック（指標のモデル）が出来たなら、法則（に相当する関数）を満たすかどうかを確認できます。法則を満たすとは、すべての状態と関連するすべての整数値に対して法則に相当する関数が真（Go言語の true）を返すことです。

法則を満たすことを保証するには無限*6の入出力を確認する必要があります。残念ながら、人間やコンピュータは無限の入出力を全数チェック出来ません。無理です。

実際に出来ることは、幾つかの個別事例について確認することだけです。例えば次のようなテスト関数です。

func TestIntStack_01(t *testing.T) {
  stack := NewIntStack()
  if !Law1_top(stack) {
    t.Error("Law1_top failed")
  }
  if !Law2_pop(stack) {
    t.Error("Law2_pop failed")
  }
  if !Law3_push(stack, 5) {
    t.Error("Law3_push failed")
  }
  if !Law4_push_top(stack, 10) {
    t.Error("Law4_push_top failed")
  }
  if !Law5_push_pop(stack, 15) {
    t.Error("Law5_push_pop failed")
  }
}

テスト関数 TestIntStack_01 が成功したからといって、それはたまたま選んだ状態と整数値に対して正しいだけのことで、スタックの当該実装が正しいとはまったく言えません。テスト関数を増やしたところで事情は変わりません。

「
ホーア論理とホーアオートマトン 1/n // プログラムの正しさを信じられる、とは？」で述べた妥当性の分類で言うと、テストにより獲得できるのは経験的妥当性です。有限個のケース〈事例〉が可能性を網羅している特別な場合なら経験的妥当性がモデル論的妥当性に一致しますが、たいていは、経験的妥当性では論理的妥当性（モデル論的妥当性／証明論的妥当性）に届きません。

なんで「プロパティ」？

最近、プロパティベーステストという言葉を聞きます。前節で、「テストでは、“たまたま選んだ事例”に対しての正しさしか確認できない」と言いました。プロパティベーステストは、“選ぶ事例”をより系統的に、より多数にするための技法です。

「プロパティベーステスト」の「プロパティ〈property〉」って何でしょうか？次のように説明されるようです。

ソフトウェア・システムが、どのような入力に対しても常に満たすべき特性／性質／ルール
ソフトウェア・システムのあるべき挙動が満たすべき条件

これは要するに、指標の法則のことです。「法則」には、「公理」「制約」「条件」などの同義語があると言いましたが、さらにもう一個「プロパティ」という同義語を追加したことになります。しかも、「プロパティ」は既に多義的に使われているポピュラーな言葉です。JSONオブジェクトの「プロパティ」はお馴染みでしょうし、知的財産は intellectual property なので、「プロパティ」は財産の意味でも使います。

どんなテストであれ、法則〈公理 | 制約 | 条件〉に対してテストを行うので、すべてのテストはプロパティベースです。テスト手法に対するネーミングとしては「いかがなものか？」と感じます。プロパティベースであること自体は、何ら特徴的ではなくて（あらゆるテストがそう）、テストデータを大量に乱数的に生成するのが“いわゆるプロパティベーステスト”の特徴のようです。

さて、オブジェクト変数 $`s`$ と整数値変数 $`v`$ を持つホーアトリプルを論理式とみなしたものを $`T(s, v)`$ と書くことにします。$`T(s, v)`$ の意味は、次のような写像です。

$`\quad t : S\times \mbf{Z} \to \mbf{B} \In \mbf{SDet}`$

$`\mbf{B}`$ に値を持つ写像は述語〈predicate〉と呼ぶので、ホーアトリプルの意味は述語です。ただし、集合圏（集合と写像の圏） $`\mbf{Set}`$ ではなくて、半決定性写像の圏 $`\mbf{SDet}`$ で考えているので、述語の値に未定義（$`\bot`$）があるかも知れません。

老婆心で言っておきますが、述語記号や論理式は構文的対象物〈syntactic object〉のことで、述語は意味的対象物〈semantic object〉です。述語記号（単なる記号・ラベル・名前）も「述語」と省略する習慣が混乱を引き起こすので注意してください。

論理式 $`T(s, v)`$ に全称記号を付けた $`\forall (s, v)\in (S\times \mbf{Z}).T(s, v)`$ の意味は、真、偽、未定義（$`\mrm{T}, \mrm{F},\bot`$）のいずれかです。$`\forall (s, v)\in (S\times \mbf{Z}).T(s, v)`$ が真であるとは次のどちらかの意味です。

弱い意味で真：半決定性写像 $`t`$ が、定義されているすべての $`(s, v)`$ において真（$`\mrm{T}`$）となる。
強い意味で真：半決定性写像 $`t`$ は決定性〈全域的〉で、すべての $`(s, v)`$ において真（$`\mrm{T}`$）となる。

ソフトウェアの記述やテストにおいては、弱い意味での真で十分です。弱い意味での真であっても、人間やコンピュータが確認できるとは限りません（ほとんど無理）。

行き当たりばったりの事例ベーステストでも、プロパティベーステストでも、（今の例で言えば）全体集合 $`S\times \mbf{Z}`$ の有限部分集合 $`K\subseteq S\times \mbf{Z}`$ を選んで、有限部分集合 $`K`$ に対する確認をしています。プロパティベーステストは、有限部分集合 $`K`$ が「より系統的、より多数（サイズが大きい）」になることが優位点です。

ホーア論理とホーアオートマトン

この記事で出した指標では、法則の記述にホーアトリプルを用いました。ホーアトリプルを論理式とみなしての構文論〈証明論〉と意味論〈モデル論〉がホーア論理〈Hoare logic〉です。ホーアトリプルを法則とする指標のモデルがホーアオートマトン〈Hoare automaton〉です。

「ホーア論理とホーアオートマトン 2/n // 単純ホーアオートマトン」で単純ホーアオートマトンを定義しました。単純ホーアオートマトンは、ラベル付き遷移系／オートマトンとの連続性もあり、ホーアオートマトンへの入口として適切だと思います。

今回の例題である“整数値を積むスタック” $`\mrm{IntStack}`$ （の実装）は、ホーアオートマトンとして定式化できます。ただし、スタック（の実装）の状態空間が、そのままホーアオートマトンの状態空間になるわけではありません。スタックを定式化するホーアオートマトンの状態空間はかなり巨大なものです。巨大な状態空間を構成するには、多項式フォック構成〈polynomial Fock construction〉を使います。これについては、引き続く記事で述べるでしょう。

「ホーア論理とホーアオートマトン 2/n // ホーアオートマトンの圏に向けて」で述べたように、単純ホーアオートマトンの圏とホーアオートマトンの圏にはだいぶギャップがあります。単純ホーアオートマトンの圏では、“オートマトンとオートマトンの結合〈composition〉”を考えてないからです。一般のホーアオートマトンの圏では、“オートマトンとオートマトンの結合”が主役となります。これについても引き続く記事で述べる予定です。

今日はここまで（「今日はここまで」参照）。

*1:例えば微積分で、余域が $`\mbf{R}`$ のときは関数、より一般的に余域が $`\mbf{R}^n`$ のときは写像と呼び分けることがあります。

*2:「同義語・多義語にホトホト困っている」では「=✗=」を使っていましたが、「≡ の否定」を表す文字がUnicodeにありました（U+2262）。

*3:同義語・多義語の問題とは別に、「シグニチャ」か「シグネチャ」か「シグニチャー」か、「インターフェイス」か「インターフェース」か「インタフェース」か、などの表記のゆれの問題もあります。

*4:より高次元の宣言まで含めるとコンピュータッド〈computad〉です。「コンピュータッドとそのモデル：同義語・類義語のジャングル」参照。

*5:状態を表す型を構造体型に限る必要はありませんが、多くの場合に構造体型が使われます。

*6:コンピュータで扱うデータ型は巨大な有限集合です。が、事実上無限です。