予測プログラミング

述語プログラミングは、プログラムの仕様記述と改良のための形式手法の元の名前であり、最近ではエリック・ヘーナーによって考案された実践的プログラミング理論と呼ばれています。中心となる考え方は、各仕様は、許容されるコンピュータの動作に対しては真、許容されない動作に対しては偽となる二値（ブール）式であるということです。したがって、改良とは単に含意に他なりません。これは最も単純で汎用的な形式手法であり、逐次プログラム、並列プログラム、スタンドアロンプ​​ログラム、通信プログラム、終了型プログラム、非終了型プログラム、自然時間プログラム、リアルタイムプログラム、決定論的プログラム、確率的プログラムに適用でき、時間と空間の制約も含まれます。

プログラミング言語のコマンドは、コンパイル可能な仕様の特殊なケースとみなされます。たとえば、プログラム変数が${\displaystyle x}$、${\displaystyle y}$、 そして${\displaystyle z}$、コマンド${\displaystyle x}$:=${\displaystyle y}$+1は仕様（二進数表現）と同等です${\displaystyle x'}$=${\displaystyle y}$+1 ∧${\displaystyle y'}$=${\displaystyle y}$∧${\displaystyle z'}$=${\displaystyle z}$その中で${\displaystyle x}$、${\displaystyle y}$、 そして${\displaystyle z}$代入前のプログラム変数の値を表し、 ${\displaystyle x'}$、${\displaystyle y'}$、 そして${\displaystyle z'}$代入後のプログラム変数の値を表します。仕様が${\displaystyle x'}$>${\displaystyle y}$我々は簡単に証明できる（${\displaystyle x}$:=${\displaystyle y}$+1) ⇒ (${\displaystyle x'}$>${\displaystyle y}$）それは、${\displaystyle x}$:=${\displaystyle y}$+1 は暗示、洗練、または実装する${\displaystyle x'}$>${\displaystyle y}$。

ループ証明は大幅に簡略化されます。たとえば、${\displaystyle x}$は整数変数であり、

その間${\displaystyle x}$>0を実行する${\displaystyle x}$:=${\displaystyle x}$-1 od

仕様を改良または実装する${\displaystyle x}$≥0 ⇒${\displaystyle x'}$=0 を証明する

もし${\displaystyle x}$>0 の場合${\displaystyle x}$:=${\displaystyle x}$–1; (${\displaystyle x}$≥0 ⇒${\displaystyle x'}$=0)それ以外の場合${\displaystyle ok}$fi ⇒ (${\displaystyle x}$≥0 ⇒${\displaystyle x'}$=0)

どこ ${\displaystyle ok}$ = (${\displaystyle x'}$=${\displaystyle x}$) は空のコマンド、つまり何も実行しないコマンドです。ループ不変条件や最小固定点は不要です。複数の中間浅い出口と深い出口を持つループも同様に動作します。この簡略化された証明形式は、プログラムコマンドと仕様を意味のある形で組み合わせることができるため可能です。

実行時間（上限、下限、正確な時間）は、時間変数を導入するだけで同じ方法で証明できます。終了性を証明するには、実行時間が有限であることを証明します。非終了性を証明するには、実行時間が無限であることを証明します。たとえば、時間変数が${\displaystyle t}$、そして時間は反復回数を数えることで測定され、前のwhileループの実行に時間がかかることを証明します。${\displaystyle x}$いつ${\displaystyle x}$最初は非負であり、${\displaystyle x}$最初は否定的であることを証明します

もし${\displaystyle x}$>0 の場合${\displaystyle x}$:=${\displaystyle x}$-1;${\displaystyle t}$:=${\displaystyle t}$+1; (${\displaystyle x}$≥0 ⇒${\displaystyle t'}$=${\displaystyle t}$+${\displaystyle x}$) ∧ (${\displaystyle x}$<0 ⇒${\displaystyle t'}$=∞)それ以外の場合${\displaystyle ok}$fi ⇒ (${\displaystyle x}$≥0 ⇒${\displaystyle t'}$=${\displaystyle t}$+${\displaystyle x}$) ∧ (${\displaystyle x}$<0 ⇒${\displaystyle t'}$=∞)

どこ${\displaystyle ok}$ = (${\displaystyle x'}$=${\displaystyle x}$∧${\displaystyle t'}$=${\displaystyle t}$)

• ECR Hehner、『プログラミングの実践理論』、Springer-Verlag、1993年。最新版は『プログラミングの実践理論』のウェブサイトで閲覧可能。

• エリック・ヘーナーの著作一覧