0

この例で、戻り値が 0 (配列に 8 がない場合) または 1 (配列に 8 がある場合) になることを証明しようとしています。

int fi8(int *array, int size) {
  int fi8 = 0;
  int i = 0;
  for(i = 0; i < length; ++i)
  {
     if(array[i] == 8)
     fi8 = 1;
  }
  return fi8;
}

そして、事前条件と事後条件を作成しました。

/*@ requires 0 <= size <= 100;
@  requires  \valid(array+(0..size-1));
@  assigns \nothing;
@  ensures (\forall integer i; 0<= i < size && array[i] != 8)  ==> (\result == 0);
@  ensures (\exists integer i; (0<= i < size && array[i] == 8)) && (\result == 1);
@*/

Frama-C は Hoare Logic に基づいているため、ループ不変条件:

/*@ loop invariant 0 <= i <= length;
  @  loop invariant  fi8 == 0 || fi8 == 1;
  @  loop invariant (\forall integer i; 0<= i < size && array[i] != 8)
      ==> (fi8 == 0);
  @  loop invariant (\exists integer i; (0<= i < size && array[i] == 8)) 
      && (fi8 == 1);
  @  loop assigns i, fi8;
  @*/

forall を使用しようとしていて、存在する行に何かが欠けていると確信しています。配列に値が割り当てられているかどうかを正しく確認する方法を理解するために何時間も費やしていますが、ここで立ち往生しているように感じます。私は本当にあなたの助けに感謝します:)

4

1 に答える 1

3

コードにはいくつかの問題があります。まず、 と が混在しているようsizeですlength。私は自由にsizeどこでも使用できるようにしました。そうしないと、このコードは C コンパイラでさえ受け入れられず、ましてや Frama-C でさえ受け入れられません。2 つ目\forall integer i; 0<= i < size && array[i] != 8(および対応するループ不変式) は正しくありません。文字通り、それは任意の整数が と の間にあるとではないの両方をi検証することを意味します。取ることは、この命題に対する自明な反例を与えます。あなたが表現したいのは、任意の整数について、が と の間にある場合、ではないということです。これは次のように表されます。i0 sizearray[i]8101ii i0size array[i]8\forall integer i; 0<= i < size ==> array[i] != 8. 一方、&&コネクタは の下で使用する場合は正しいです\exists。今回は、配列の境界内にあり、その対象となるものiを実際に見つけたいと考えています。ただし、最後の保証の2番目は正しくありません。あなたが言いたいのは、そのような がある場合、、したがって、ここに意味がなければならないということです。iarray[i]==8&&i\result == 1(\exists integer i; 0<= i < size && array[i] == 8) ==> (fi8 == 1)

最後の問題は、ループの不変条件にあります。既に C 変数であるにもかかわらず、数量化された変数として再利用していますが、これは多くの場合、良い考えではありません。実際、表現したいプロパティは、 と の8間が見られない限り (0そしてi,fi8==0が見られた8場合fi8==1)、iC 変数であることであるため、これは実際の問題です。j次のように、定量化で使用する場合

 loop invariant (\forall integer j; 0<= j < i ==> array[j] != 8) ==> (fi8 == 0);
 loop invariant (\exists integer j; 0<= j < i && array[j] == 8) ==> (fi8 == 1);

すべての立証義務が免除されます。

于 2014-11-23T17:10:55.697 に答える