#はじめに
ある証券会社のサイトの証券用語「板寄せ」の解説にあったアルゴリズムに対して、実装バグ、すなわち「仕様を満たさない入力」が存在しないことを数学的に検証する形式検証を行ないました。
すると、実はその解説にはそもそも仕様バグ、すなわち「仕様そのものの間違い」が存在していることが分かりました。
そこで本記事では、元の解説の「仕様」に対してどこに仕様バグがあるのか、どのように改善すればいいのかを解説していきます。
※私はフィンテックが独学であるため、専門用語の言い回しなどが稚拙な箇所があるかもしれません。あらかじめご了承ください。
#ある証券会社の証券用語の解説
本記事が参考にした板寄せアルゴリズムの解説は楽天証券/現物取引 取引ルール/板寄せですが、他にもマルサントレード/板寄せとは？などのサイトでも同じ仕様が記述されていました。
##掲載されていた仕様
板寄せアルゴリズムが満たすべき仕様を引用したものが以下の3つです。
3つの条件を満たす値段で売買が成立
【条件1】
成行の売り注文と買い注文すべてについて約定すること
【条件2】
約定値段より高い買い注文と、約定値段より低い売り注文がすべて約定すること
【条件3】
約定値段において、売り注文または買い注文のいずれか一方すべてについて約定すること
一見良さそうに見えますが、実はこの仕様は間違いで、特に、正しい板寄せアルゴリズムはこれを満たさないことが分かりました。
例えば、注文が成行の売り注文のみで買い注文が全くない場合、約定しようがないので条件１を満たしません。
よって、任意の入力に対して仕様を満たす出力が存在する訳ではないので、仕様バグが存在していると言えます。
##もう一つの問題点
実はこの仕様にはもう一つ大きな問題があります。
それは「正しい約定」が定義されていないことです。
そのため、例えば「全ての注文に対して、それと価格と注文数の等しい架空の逆注文を勝手に追加して、これら同士を約定させることによって全ての注文が約定する」というはちゃめちゃなアルゴリズムでも上記の仕様を全て満たしてしまいます。
つまり、この３つのみの仕様では「形式検証で保証できることは何か？数学的に捉えて見えてきたこと」の例のように仕様が設計通りに十分に記述できていないため、形式検証して実装バグが存在しないことを示せたとしても、仕様にはない予期せぬバグが発生している可能性があるということです。
そこで、本記事ではもう一度、板寄せアルゴリズムが満たすべき仕様を考えます。
#「板寄せ」の仕様を再定義する
板寄せの仕様を正しい形に再定義します。
まずは掲載されていた3つの仕様を再定義します。
##掲載されていた仕様を再定義
###条件1
【条件1】
成行の売り注文と買い注文すべてについて約定すること
- [条件1] **未約定(売り/買い)注文が存在するならば、**未約定(買い/売り)注文は全て指値である。
売り注文か買い注文のどちらかが空であり、かつ成り行き注文が余る場合に満たさなくなるので、この場合を排除します。
###条件2
【条件2】
約定値段より高い買い注文と、約定値段より低い売り注文がすべて約定すること
- [条件2] 約定値段が存在するならば、全ての指値の未約定(売り/買い)注文の価格は約定値段より(高い/低い)か等しい。
約定価格が存在しない、すなわち全てが成行注文である等、約定価格を設定できる注文が1つもない場合を考慮しました。また、この命題をのちに形式検証する都合上、対偶の形をとっています。
###条件3
【条件3】
約定値段において、売り注文または買い注文のいずれか一方すべてについて約定すること
- [条件3] **約定値段が存在するならば、**未約定の売り注文か買い注文のうちどちらか全ての指値価格は約定価格と異なる。
条件3も約定価格が存在しない場合を考慮しました。
条件を書き換えましたが、この仕様ならば板寄せアルゴリズムが満たすことが証明できます。詳細は実際に形式検証を行った実装編の記事をご覧ください。
##追加の仕様
しかしながら、上で再定義した仕様だけでははちゃめちゃなアルゴリズムでも満たしてしまうため、不十分です。
そこで、板寄せアルゴリズムが満たすべき追加の仕様を考えます。
###約定価格の存在性
まず、約定価格が存在しない場合が考えられるので、その必要十分条件を定義します。
-
[約定価格の存在性] 約定価格が存在することは以下のどちらかが成り立つことと同値である。
- 約定価格の初期値が設定されていること。
- 指値注文が存在すること。
約定価格が存在しない場合は、前の日の終値に設定するなどの方法が考えられるので、それを初期値としました。
指値注文が1つでもあれば約定しなくても価格が設定できると考え、このような定義になっています。
つまり、この命題が表すのは、約定価格が存在しないときは、約定価格の初期値が設定されていないかつ、指値注文が1つもないときのみということです。
###約定の注文数
注文における注文数に対しても制約がなければいけません。
- [約定の健全性1] **任意の注文者に対し、**その注文者による(売り/買い)注文の注文数の合計と、その注文者の約定した(売り/買い)注文及び未約定の(売り/買い)注文の注文数の合計が一致する。
ここで、「任意の注文に対し」ではなく、「任意の注文者に対し」になっているのは、元の注文には存在しない第三者による注文が新たに追加されたりしないことも意味しています。
特に健全性1は注文数に関する制約で、発注した取引数と約定した取引としなかった取引の合計数が等しいことを表しています。
###約定の価格
- [約定の健全性2] **任意の注文者に対し、**その注文者による指値(売り/買い)注文が存在し、同じ注文者の約定した(売り/買い)注文が存在する場合、その価格は元の注文の価格に等しいまたは(高い/安い)。
健全性2は価格に関する制約です。指値注文が約定した場合、その価格よりも良い取引になっている必要があることを表しています。ここで、「指値価格で約定すること」と定義していないのは、板寄せアルゴリズムにおいて、価格の異なる売り注文と買い注文を約定させる場合があるからです。
他にも考えられる仕様があるかも知れませんが、これらの追加の仕様によって、少なくても架空の注文が追加されたり勝手に注文が削除されたりしないことを保証することができます。
また、上記の追加した仕様に対しても板寄せアルゴリズムが満たすことの証明は次の記事「株式の取引と売買価格を決定する板寄せアルゴリズムをCoq/SSReflectで形式検証する」に記載しています。詳細はそちらをご覧ください。
#まとめ
ある証券会社の証券用語解説の「板寄せ」の解説における仕様の間違いを形式検証の視点から発見しました。
仕様を考えるときには、任意の入力に対して成り立つようなものにしなくてはならず、また、それら全ての仕様を満たすはちゃめちゃなアルゴリズムが考えられないかも考察する必要があることが分かりました。
形式検証によってバグを発見した別の記事
「形式検証の視点から再確認したいMaybe型/Option型から許容データベースへのデータ変換」