線形探索アルゴリズムの正当性、停止性の証明

Question

前提・実現したいこと

teratail初心者のため失礼がありましたら申し訳ございません。
院試の勉強をしており、以下の線形探索アルゴリズムの正当性、停止性を証明して頂きたいです。

該当のソースコード

#include <stdio.h>
#define N 9 /*探している値*/

int main(void){
  int a[10]={3,10,4,5,6,1,8,7,9,2};
  int number=sizeof(a)/sizeof(int);

  int i;

  for(i=0; i<number; i++){
    if(N==a[i]){
      printf("%d番目に見つかりました\n", i+1);
      return 0;
    }
  }
  printf("見つかりませんでした\n");
  return 0;
}

試したこと

停止性の自分で出した証明↓↓↓
forの繰り返しはi=numberになったらループを抜けるため、このプログラムは停止する。

正当性はわからないので教えて頂きたいです。停止性もこんな単純でいいのかと不安です。
よろしくお願いいたします。

Answer 1

• 以下の線形探索アルゴリズムの正当性、停止性を証明して頂きたいです。

停止性の証明はegproが書かれていることで概ねあっています。
厳密にいえば、for文の本体であるブロックの中で変数iの更新がないことを明記しておけばよろしいでしょう。

正当性の証明はできません。
その理由は、「仕様」が書かれていないからです。

もしも、このプログラムの仕様が

「9番目に見つかりました」と表示した後で改行する」

であれば正当です。ただし、

#include <stdio.h>
int main(void){
    printf("9番目に見つかりました\n");
}

も同じように正当です。

もしも、このプログラムの仕様が

任意の長さの整数配列から指定した整数と一致する要素がある場合に、その要素の最も小さいインデックス＋１を使って「番目に見つかりました」と表示した後で改行する。
一致する要素があるない場合は「、見つかりませんでした」と表示した後で改行する。

であれば、正当ではありません。
それは、整数配列の要素が2147483649以上であったり、配列の長さが2147483649以上である場合は仕様通りに動作しないからです。

Answer 2

私は趣味&独学なので詳しくはわかりません。

ですが、『アルゴリズム 正当性 証明』でggると、こちらがヒットしました。

上記を読むに、『実際のデータを入れてみて、本来の結果になるか』を流れでやってみるだけのようです。

[例]

n = 1のとき、int x = 3 ＊ n + 1は

3×1×1=3

n = 2 のとき、...

したがってこのアルゴリズムは正当である。

的な感じでは？

(上記はあくまで例。もっとましなフォーマットがあればそれに従うべきですね。私は無学なので)