ACSL Mini Tutorial

PDF-файл ACSL Mini Tutorial Формальная спецификация и верификация программ (64210): Книга - 9 семестр (1 семестр магистратуры)ACSL Mini Tutorial: Формальная спецификация и верификация программ - PDF (64210) - СтудИзба2020-08-21СтудИзба

Описание файла

PDF-файл из архива "ACSL Mini Tutorial", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст из PDF

ACSL Mini-TutorialVirgile Prevosto11CEA LIST, Software Security Laboratory, Saclay, F-91191This work has been partially supported by the CAT ANR project (ANR-05-RNTL-0030x) and by the FP6European project Open TC.Chapter 1ForewordThis document is a brief introduction to the ANSI/ISO C Specification Language (ACSL). ACSL allows to formallyspecify the properties of a C program, in order to be able to formally verify that the implementation respects theseproperties. This verification is done via tools that are able to take into account ACSL annotations attached to the Ccode. This tutorial focuses on the most important ACSL constructs and gives an intuitive grasp of their semantics,through short and illustrative examples of C code annotated with ACSL formulas. A complete reference of theACSL language can be found in [1].

ACSL is inspired from the specification language used by Caduceus [2],which is itself derived from the Java Modeling Language (JML, see [3]).Chapter 2A First ACSL ExampleThe most important ACSL concept is the function contract. A function contract for a C function f is a set ofrequirements over the arguments of f and/or a set of properties that are ensured at the end of the function.

Theformula that expresses the requirements is called a pre-condition, whereas the formula that expresses the propertiesensured when f returns is a post-condition. Together, these conditions form a contract between f and its callers:each caller must guarantee that the pre-condition holds before calling f. In exchange, f guarantees that the postcondition holds when it returns.Let us consider the example of the max function. Informally, its specification can be expressed this way: thefunction max takes two int as arguments, and returns the greatest one.

Let us see how this can be expressed inACSL:/*@ ensures \result >= x && \result >= y;ensures \result == x || \result == y;/*int max (int x, int y) { return (x > y) ? x : y; }As can be seen above, ACSL annotations are written in special C comments, the difference with plain commentsbeing that annotations begin with ’/*@’. It is also possible to write one-line annotations introduced by ’//@’. Thefunction contract is written immediately above the function declaration.

In this example, the contract contains onlypost-conditions (ensures clauses), as max does not have any particular requirement. The first ensures clauseexpresses the fact that the result of max is greater than both x and y, the arguments of max. The second clausemandates that the result is equal to either x or y. Since both clauses must hold, our ACSL specification indeedexpresses that the result of max is the greatest of its two arguments.It should be noted already that there is an intuitive demarcation between “complete” and “partial” specifications.

The above specification for max can be thought of as “complete”, meaning that any function that satisfiesthe specification should be deemed a satisfactory implementation for max. Partial specifications on the other handexpress some of the properties that are expected to hold for any implementation, but satisfying them is not sufficient for an implementation to be satisfactory. Generally speaking, partial formal specifications are the most likelyto be encountered in practice for real-life examples, complemented by informal specifications. For instance, theabove specification for max is in fact partial, for reasons that will become clearer later.Chapter 3Pointers3.1A First SpecificationLet us now consider a small program involving pointers. Informally, the max_ptr function takes two pointers asargument, and if necessary swaps the two pointed values so that the value stored in the first pointer is the minimalone and the value stored in the second pointer is the maximal one.

A specification can be the following:/*@ requires \valid(p) && \valid(q);ensures *p<=*q;*/void max_ptr(int *p, int* q);Here, we have a pre-condition (the requires clause). Namely, we want our function to be called withvalid pointers as arguments. This is what the built-in ACSL predicate \valid says. Note that \valid takesinto account the static type of its argument: in our context, \valid(p) indicates that there address p is included in an allocated block which is large enough to store an int starting at p. This is thus different from\valid((char *)p) for instance.Our post-condition is that when the function returns, the value pointed to by p is less than or equal to the valuepointed to by q.A correct implementation for max_ptr is thenvoid max_ptr(int*p, int*q) {if (*p > *q) {int tmp = *p;*p = *q;*q = tmp;}}Namely, since we require max_ptr to be called with valid pointers, there is no need to perform any check onthem.

Then, if *p is already less than or equal to *q, there’s nothing to do. If not, we just swap the content of thetwo pointers.3.2Building a Complete SpecificationThe implementation seen in the previous section is correct with respect to the specification of max_ptr. Unfortunately, this is not the only conforming implementation: the specification is only partial, and is for instance metby the following function:void max_ptr(int* p, int*q) {*p = *q = 0;}3.3 Degree of CompletenessIndeed, since 0 ≤ 0, we have *p<=*q at the end of the function.Depending on the verification tasks we have in mind (see next section), we may want to refine our specificationto avoid an implementation such as above.

Namely, we want to enforce a relation between the values pointed to byp and q at the beginning and at the end of the function. A possible specification is then/*@ requires \valid(p) && \valid(q);ensures *p <= *q;ensures (*p == \old(*p) && *q == \old(*q)) ||(*p == \old(*q) && *q == \old(*p));*/void max_ptr(int* p, int*q);The \old built-in function says that its argument must be evaluated in the pre-state (i.e.

at the beginning) of thefunction. The second ensures clauses thus says that we either leave p and q unchanged or swap the two pointedvalues, which, together with the first clause implies that we meet exactly the informal specification.3.3Degree of CompletenessThe previous section has teached us that writing a fairly complete specification (in fact we could still add someclauses to the specification above, as we will see in the next chapters) is not immediate, and thus that it is easy tocome up with only a partial specification.

Hence, it raises two frequently asked questions: how can we be sure thatour specification is complete, and how complete must a specification be.The answers however do not lie in ACSL itself. For the first one, one must reason on some model of thespecified application. For the second one, there is no definite answer. It depends on the context in which thespecification is written and the kind of properties that must be established: the amount of specification requiredfor a given function is very different when verifying a given property for a given application in which calls tothe function always occur in a well-defined context and when specifying it as a library function which should becallable in as many contexts as possible.4Chapter 4BehaviorsThe second ensures clause of our final specification of max_ptr is a bit complicated, and does not explainimmediately in which case we will end up.

It is possible to express that differently, by using ACSL’s behaviors. A function can have several behaviors in addition to a general specification. A behavior can have additionalensures clauses, but in addition, it can also have assumes clauses, which indicate when the behavior is triggered. There is no requirement for the behaviors to cover all contexts in which a function can be called, andbehaviors need not to cover disjoint cases. This can be further specified by the complete behaviors anddisjoint behaviors clauses, as in the following specification./*@ requires \valid(p) && \valid(q);ensures *p <= *q;behavior p_minimum:assumes *p < *q;ensures *p == \old(*p) && *q == \old(*q);behavior q_minimum:assumes *p >= *q;ensures *p == \old(*q) && *q == \old(*p);complete behaviors p_minimum, q_minimum;disjoint behaviors p_minimum, q_minimum;*/void max_ptr(int* p, int*q);We explain here precisely in which case we keep the same values and in which case we swap.

Note that theglobal ensures clause is implied by the ensures clauses of the two behavior and the fact that p_minimumand q_minimum form a complete set of behaviors.Chapter 5Arrays5.1Basic SpecificationNow that we have specified a max_ptr function, we can use it to extract the maximal value found in a sequenceof ints. A first step is to write the prototype of the corresponding function with its specification./*@ requires n > 0;requires \valid(p+ (0..n−1));ensures \forall int i; 0 <= i <= n−1 ==> \result >= p[i];ensures \exists int e; 0 <= e <= n−1 && \result == p[e];/*int max_seq(int* p, int n);The function takes two arguments: a pointer p to the block containing the ints, and the number n of elementsin the sequence. This time, there are pre-conditions on these arguments. First, it is not possible to compute themaximal value of an empty sequence, and so n must be positive.

Свежие статьи
Популярно сейчас
Зачем заказывать выполнение своего задания, если оно уже было выполнено много много раз? Его можно просто купить или даже скачать бесплатно на СтудИзбе. Найдите нужный учебный материал у нас!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее