design-by-contract - ACSL 后置条件中\old 的含义

Question

我是 Frama-C 的新手，有几个关于断言的问题 在指针上。

考虑下面的 C 代码片段:

• 两个相关的数据结构Data和Handle，s.t.句柄有一个指向数据的指针；
• 数据中的“状态”字段，指示某些假设操作是否已完成
• 三个函数:init()、start_operation()和wait()；
• 使用上述内容的 main() 函数，包含 6 个断言 (A1-A6)

现在，为什么 A5 和 A6 不能用 WP 验证器断言(“frama-c -wp file.c”) 由于 start_operation() 上的最后一个“确保”子句，它们不应该成立吗？

我做错了什么？

最好的，

爱德华多

typedef enum 
{ 
  PENDING, NOT_PENDING
} DataState;

typedef struct 
{
  DataState state;
  int value;  
} Data;


typedef struct 
{
  Data* data;
  int id;
} Handle;

/*@
  @ ensures \valid(\result);
  @ ensures \result->state == NOT_PENDING;
  @*/
Data* init(void);

/*@ 
  @ requires data->state == NOT_PENDING;
  @ ensures data->state == PENDING;
  @ ensures \result->data == data;
  @*/  
 Handle* start_operation(Data* data, int to);

/*@
  @ requires handle->data->state == PENDING;
  @ ensures handle->data->state == NOT_PENDING;
  @ ensures handle->data == \old(handle)->data;
  @*/  
 void wait(Handle* handle);


 int main(int argc, char** argv)
 {
  Data* data = init();
  /*@ assert A1: data->state == NOT_PENDING; */

  Handle* h = start_operation(data,0);
  /*@ assert A2: data->state == PENDING; */
  /*@ assert A3: h->data == data; */

  wait(h);
  /*@ assert A4: h->data->state == NOT_PENDING; */
  /*@ assert A5: data->state == NOT_PENDING; */
  /*@ assert A6: h->data == data; */

  return 0; 
}

Answer 1

您正在为“新手”验证一些棘手的内存操作。

ACSL 构造 \old 并不像您想象的那样工作。

首先，后置条件中的\old(handle)与handle是一样的，因为handle是一个参数。契约(Contract)旨在从调用者的角度使用。即使函数 wait 修改了 handle(这不常见但有可能)，它的契约仍然旨在将调用者作为参数传递的值与返回的状态相关联通过函数传递给调用者。

简而言之，在 ACSL 后置条件中，parameter 始终表示 \old(parameter)(即使函数修改了 parameter 就像一个局部变量)。

其次，上述规则仅适用于参数。对于全局变量和内存访问，后置条件被认为适用于后置状态，正如您从其名称中所期望的那样。您编写的构造 \old(handle)->data 等同于 handle->data，表示“字段 .data handle 的旧值指向新状态”，因此后置条件 handle->data ==\old(handle)->data 是重言式，可能不是你想要的有意的。

从上下文来看，您似乎打算改为使用 handle->data ==\old(handle->data)，这意味着“字段 .data handle在新状态下指向的旧值等于handle在旧状态下指向的字段.data状态”。有了这个改变，你程序中的所有断言都得到了证明(使用 Alt-Ergo 0.93)。