ACSL后置条件中\ old的含义 [英] Meaning of \old in ACSL post-conditions

问题描述

我是Frama-C的新手用户，并且对断言有一些疑问 指针上方.

I am a newbie user of Frama-C and have a few questions regarding assertions over pointers.

考虑以下涉及的C片段:

Consider the C fragment below involving:

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

现在，为什么不能用WP验证程序来断言A5和A6("frama-c -wp file.c") 他们不应该因为start_operation()的最后一个确保"子句而持有吗?

Now, why is it that A5 and A6 cannot be asserted with the WP verifier ("frama-c -wp file.c") Shouldn't they hold due to the last "ensures" clause on 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; 
}

推荐答案

您正在验证新手"的一些棘手的内存操作.

You are verifying some tricky memory manipulations for a "newbie".

ACSL构造\old的工作方式与您认为的完全不同.

The ACSL construct \old does not work exactly like you think it does.

首先，后置条件中的\old(handle)与handle相同，因为handle是参数.从呼叫者的角度出发，应使用合同.即使功能wait修改了handle(这是不寻常的，但可能的)，它的协定也仍然打算将调用者作为参数传递的值和该函数返回给调用者的状态联系起来.

First, \old(handle) in a post-condition is the same as handle, because handle is a parameter. A contract is intended to be used from the point of view of callers. Even if the function wait modified handle (which would be unusual but is possible), its contract would still be intended to relate values passed as argument by the caller and the state returned by the function to the caller.

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

In short, in an ACSL post-condition, parameter always means \old(parameter) (even if the function modifies parameter like a local variable).

第二，以上规则仅适用于参数.对于全局变量和内存访问，后置条件被认为适用于后置状态，正如您期望的那样.您编写的与handle->data等效的结构\old(handle)->data表示句柄的旧值在新状态下指向的字段.data"，因此后置条件handle->data == \old(handle)->data为重言式，可能不是您想要的.

Second, the rule above is only for parameters. For global variables and memory accesses, the post-condition is considered to apply to the post-state, as you would expect from its name. The construct \old(handle)->data that you wrote, and that is equivalent to handle->data, means "the field .data that the old value of handle points to in the new state", so that the post-condition handle->data == \old(handle)->data is a tautology and probably not what you intended.

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

From the context, it appears that you intended handle->data == \old(handle->data) instead, which means "the field .data that the old value of handle points to in the new state is equal to the field .data that the old value of handle points to in the old state". With that change, all the assertions in your program get proved for me (using Alt-Ergo 0.93).

这篇关于ACSL后置条件中\ old的含义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！