Значение \ old в постусловиях ACSL - PullRequest
Новая
       15

Значение \ old в постусловиях ACSL

3 голосов
/ 29 марта 2012

Я новичок в Frama-C и у меня есть несколько вопросов относительно утверждений над указателями.

Рассмотрим фрагмент C ниже, включающий:

  • две связанные структуры данных.Handle, st. Handle имеет указатель на Data;
  • поле 'state' в Data, указывающее, завершена ли какая-либо гипотетическая операция
  • три функции: 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; 
}

1 Ответ

2 голосов
/ 30 марта 2012

Вы проверяете некоторые хитрые манипуляции с памятью для «новичка».

Конструкция ACSL \old работает не совсем так, как вы думаете.

Во-первых, \old(handle) впостусловие совпадает с handle, потому что handle является параметром.Контракт предназначен для использования с точки зрения абонентов.Даже если функция wait изменила handle (что было бы необычно, но возможно), ее контракт по-прежнему должен был бы связывать значения, передаваемые вызывающей стороной в качестве аргумента, и состояние, возвращаемое функцией вызывающей стороне.

Вкратце, в постусловии ACSL, parameter всегда означает \old(parameter) (даже если функция изменяет parameter как локальная переменная).

Second,Правило выше только для параметров.Для глобальных переменных и обращений к памяти пост-условие считается применимым к пост-состоянию, как и следовало ожидать от его имени.Написанная вами конструкция \old(handle)->data, эквивалентная handle->data, означает «поле .data, на которое указывает старое значение handle в новом состоянии», так что постусловие handle->data == \old(handle)->data являетсятавтология и, вероятно, не то, что вы намеревались.

Из контекста выясняется, что вы вместо этого намеревались handle->data == \old(handle->data), что означает "поле .data, на которое указывает старое значение handle в новом состоянии.равно полю .data, на которое указывает старое значение handle в старом состоянии ». С этим изменением все утверждения в вашей программе будут доказаны для меня (используя Alt-Ergo 0,93).

...