さてさて、ちょっと検証の本質に近づいて行きます。今度はプロセスのステップ数です。式を１つ評価するごとに１ステップとなります。上記の例はa=0;が第1ステップ、b=0;が第2ステップ、c=a;は第３ステップ、c=1は第4ステップとなります。この場合4ステップで終了となります。もし、SPINが『全ての変数(a,b,c)が0になることがある』という検証しようとします。このとき、SPINはコードの最初から順番にステップを追っています。第3ステップに達したところで全ての値が0になったので、この検証はvalidであると評価します。