4

Frama-c の WP プラグインを使用して、単純なアサーションを証明しようとしています。C コードは、Targetlink ルックアップ テーブルから生成されました。私の目的は、結果のコントラクトを使用して呼び出しプログラムのプロパティを証明できるように、関数に十分な注釈を提供することです。最初のステップとして、関数の先頭付近にアサーションを記述しました。このアサーションは、定数を参照解除されたポインターから取得した値と比較します。次の例を参照してください。

typedef struct MAP_Tab1DS0I2T3_b_tag {
   int Nx;
   const int * x_table;
   const int * z_table;
} MAP_Tab1DS0I2T3_b;

int LARA_GearEnaCndn_X[9] =
{
   -1, 0, 1, 2, 3, 4, 5, 6, 8
};

int LARA_GearEnaCndn_Z[9] =
{
   1, 0, 1, 1, 0, 0, 0, 0, 0
};


MAP_Tab1DS0I2T3_b Sb218_LARA_GearEnaCndn_CUR_map = {
   9,
   (const int *) &(LARA_GearEnaCndn_X[0]),
   (const int *) &(LARA_GearEnaCndn_Z[0])
};

/*@ requires x == 2; */
int Tab1DS0I2T3_b(const MAP_Tab1DS0I2T3_b * map, int x)
{
   /* SLLocal: Default storage class for local variables | Width: 8 */
   int Aux_U8;
   int Aux_U8_a;
   int Aux_U8_b;
   int Aux_U8_c;

   /* SLLutLocalConst: Default storage class for local variables | Width: 32 */
   const int * x_table /* Scaling may differ through function reuse. */;
   const int * z_table /* Scaling may differ through function reuse. */;

   x_table = map->x_table;
   z_table = map->z_table;

   //@ assert (x < x_table[(int) (map->Nx - 1)]);

   if (x <= *(x_table)) {
      /* Saturation. */
      return z_table[0];
   }
   if (x >= x_table[(int) (map->Nx - 1)]) {
      return z_table[(int) (map->Nx - 1)];
   }

   /* Linear search, start low. */
   x_table++;
   while (x > *(x_table++))    {
      z_table++;
   }
   x_table -= 2 /* 2. */;
   Aux_U8 = *(z_table++);
   Aux_U8_a = *(z_table);

   /* Interpolation. */
   Aux_U8_b = (int) (((int) x) - ((int) x_table[0]));
   Aux_U8_c = (int) (((int) x_table[1]) - ((int) x_table[0]));
   if (Aux_U8 <= Aux_U8_a) {
      /* Positive slope. */
      Aux_U8 += ((int) ((((int) (int) (Aux_U8_a - Aux_U8)) * ((int) Aux_U8_b)) /
       Aux_U8_c));
   }
   else {
      /* Negative slope. */
      Aux_U8 -= ((int) ((((int) (int) (Aux_U8 - Aux_U8_a)) * ((int) Aux_U8_b)) /
       Aux_U8_c));
   }
   return Aux_U8;
}

誰かが証明で成功するために必要な注釈を教えてもらえますか? Coq の証明義務を見てみると、「addr_of_data」や「access」など、用語を書き直すために必要な操作の公理がないことがわかります。また、アサーションで参照されているグローバル変数の情報も欠落しています。

1 subgoals
______________________________________(1/1)
forall x_0 map_0 : Z,
is_sint32 x_0 ->
forall m_0 : array data,
x_0 = 2 ->
forall x_table_0 : Z,
x_table_0 = addr_of_data (access m_0 (addr_shift map_0 1)) ->
2 <
sint32_of_data
  (access m_0
     (addr_shift x_table_0
    (as_sint32 (sint32_of_data (access m_0 (addr_shift map_0 0)) - 1))))

BR、ハラルド

4

1 に答える 1

4

addr_of_data、addr_shiftなどの exiom は、coq-ide の store_model.v タブで自動的に与えられます。

あなたの例では、マップが実際のパラメーターとしてSb218_LARA_GearEnaCndn_CUR_mapを取得するとはどこにも述べていません 。それがなければ、主張は間違っている可能性があります。

今、証明の一部としてwpにグローバル初期化子の明示的な値を利用させる方法がわかりません。ACSL にはいくつかのグローバルな不変条件がありますが、 wpはとにかくそれらを処理していないようです。したがって、必要な値に対して明示的なrequireステートメントを使用します。

関数ヘッダーに次の一連のステートメントがあるとします。

/*@ requires x == 2; 
    requires map->x_table == Sb218_LARA_GearEnaCndn_CUR_map.x_table;
    requires map->Nx == Sb218_LARA_GearEnaCndn_CUR_map.Nx;
    requires LARA_GearEnaCndn_X[8] == 8;
    requires Sb218_LARA_GearEnaCndn_CUR_map.Nx == 9;
    requires Sb218_LARA_GearEnaCndn_CUR_map.x_table == LARA_GearEnaCndn_X;
    requires Sb218_LARA_GearEnaCndn_CUR_map.z_table == LARA_GearEnaCndn_Z;
*/

必要なアサーションを証明できました。

最初のものはあなたのものです。2 番目と 3 番目のものは*map=Sb218_LARA_GearEnaCndn_CUR_map 、アドレス範囲を台無しにしないための明示的な展開です。残りは初期化子の値を反映しています。

于 2012-12-19T04:37:02.380 に答える