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

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

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

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

formal-verification frama-c design-by-contract
person edrdo    schedule 29.03.2012    source источник
comment
Я добавил к вопросу теги формальная проверка и дизайн по контракту. Если последователи этих тегов возражают против такого рода вопросов, вините меня, а не ОП. Я не добавил тег C, потому что ожидаю, что большинство программистов на C не обратят на них внимания. Возможно, я ошибаюсь - очевидно, что многих людей не волнует, интересны ли их вопросы с тегами C.   -  person Pascal Cuoq    schedule 30.03.2012

Ответы (1)


arrow_upward
2
arrow_downward

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

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

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

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

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

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

person Pascal Cuoq    schedule 29.03.2012
comment
Да, вы поняли мои намерения. Используя handle- ›data == \ old (handle-› data), он работает. Большое спасибо. - person edrdo; 30.03.2012