「占い、テスト、エラーの修正」という周期的な方法を使用したくない場合は、ループ不変条件なしでは実行できません。
ループ不変式は、ループの前にtrue、ループの間にtrue、ループを終了したときにtrueになる関係です。 これはすべて、「プログラミングの規律」という本でダイクストラによって説明され、「プログラミングの科学」という本でグリスによって詳細にかみ砕かれています。 それにもかかわらず、私の観察によれば、実際には、この方法は誰も実際には使用していません。 これは大きな間違いです。
ベントレー自身c。 51は、次の不変式を提供します。「要素Tが配列X [1..N]にある場合、Xに属するドメインにある必要があります」。 最初は、この領域はアレイ全体です。
この言い回しはかなり不明瞭です。 この理由は、Bentleyにはほとんど経験がないためだと思います。多くの人と同様、彼はこの理論全体を実習ではなくトレーニングにのみ使用しています。
ベントレーの本を読んだとき（かなり前）、「あなたが信じているように-今すぐこの本を延期し、自分でプログラムを書きましょう」という言葉に達したとき、私は本を閉じてすぐに普通の言葉を見つけました。
配列の端に領域Oを定義して、目的の要素Tが含まれないようにします。これは、サイクルの不変式です：「領域Oは、求められた要素Tを含みません」。
最初に、この領域は、配列の先頭と末尾にある、長さゼロの2つの隣接していない部分（厚みがある場合）で構成されます。 空であり、何も含まれていないため、必要な要素は含まれていません。
作業中にこの領域が配列全体をカバーしている場合、問題の要素は配列内にありません。
形式表記（文字と配列次元1..NはBentleyの場合と同様）：
Aj：1 <= j <LまたはU <j <= N：X [j]！= T
最初は、L = 1、U = N、エリアは空です。
エリアはいつアレイ全体をカバーしますか？ L> Uの場合、セルごとに描画して確認できます。 この条件は、ループを終了するために使用されます。
次に、ループの内容について説明します。 配列Xの中央の要素（インデックスをMで表す）が目的の要素Tと等しくないと仮定します。不変式がtrueのままになるようにLとUを変更するにはどうすればよいですか？ このような定式化では、タスクは非常に単純であるため、ミスをする場所はありません。 Tが中間要素よりも大きい場合、1から中間要素までのピース全体にTはありません。同様に、Tが中間要素よりも小さい場合、中間要素からNまでのピース全体にTはありません。領域は最初の場合L：= M + 1 、2番目のU：= M-1
アルゴリズムのすべての主要な点、つまり、ループを終了する条件「L> U」（継続するには「L <= U」の否定）、領域の境界L：= M + 1、U：= M- 1私たちは、占いではなく、厳密でありながら非常に単純な推論によって推論しました。
結果の擬似コードアルゴリズムは次のとおりです。
L：= 1; U：= N; 見つかった：= false;
while（L <= U）＆not found do
M：=セグメントL..Uの中点;
[M] = Tの場合
見つかった：= true;
elseif a [M] <T then
L：= M + 1;
他に
U：= M-1;
終わり;
終わり