Prolog で実装するモデル検査器の心臓部 - Qiita

この記事では Prolog を使ったモデル検査器の実装を紹介します。 モデル検査器は、プログラムやアルゴリズムについて主に次の2つの性質の検証を目的としています： 望ましい状態にいつかなる たとえば、いつかロックを獲得できる、いつか全ノードの状態が一致する、… 望ましくない状態に陥らない たとえば、デッドロックにならない、結果が不定にならない、… 上記の性質の検証はいずれも従来のテストでは難しく、ここにモデル検査が活躍できる余地があります。このうち、今回はデッドロックを検知するプログラムを実装します。 このプログラムでは、検査対象のプログラムやアルゴリズムの取りうる状態を洗い出し、ここにまずいものが含まれていないことを検査します。まずは状態の洗い出しから説明します。 状態の洗い出し 今回の実装ではプログラムの状態を変数と実行位置の2つに絞り、これらの変化を調べていきます。 たとえば、以下の

[devorgachem]

書きました