1. На языке ACSL напишите спецификацию для следующей функции: int modify(int *data, size_t sz); согласно приведенным ниже требованиям. Предложите реализацию для этой функции и докажите ее полную корректность относительно спецификации.

    Функция получает на вход массив размера sz. Функция меняет местами некоторые два элемента массива и возвращает 0. Если ей это не удается, она возвращает некоторое ненулевое значение. Ничего другого функция делать не может.

  2. Вам дан заголовочный файл queue.h. Он содержит определения типов данных и заголовки функций для работы с очередями целых чисел. Ниже приведены требования к типу данных и функциям. Вам нужно формализовать эти требования в виде спецификации на языке ACSL и записать ее в заголовочном файле.

    Обратите внимание на то, что требования допускают множество реализаций. Внимательно отразите требования в формальной спецификации.

    Требования: очередь целых чисел хранится в массиве buffer размера capacity как часть непрерывная часть массива размера count, начиная с индекса start. Элементы извлекаются из очереди из минимального индекса подмассива. Элементы добавляются в очередь к максимальным индексам подмассива.

    Все функции возвращают 0 в случае успеха и ненулевое значение в случае неуспеха.

    Функция Queue__initialize выделяет динамическую память для buffer размера size. Размер очереди делается равным 0. Если функция не может это сделать, она возвращает ненулевое значение.

    Функция Queue__finalize освобождает динамическую память под buffer. Если функция не может это сделать, она возвращает ненулевое значение.

    Функция Queue__enqueue дополняет подмассив справа значением item. Если функция не может это сделать, она возвращает ненулевое значение. Функции разрешается менять содержимое queue, если это не отражается на ее очереди. Функции не разрешается менять какую-либо память, кроме памяти под очередь.

    Функция Queue__dequeue записывает по валидному указателю item элемент с минимальным индексом в подмассиве и удаляет его из очереди, если очередь непуста. Если функция не может это сделать, она возвращает ненулевое значение. Функции разрешается менять содержимое queue, если это не отражается на ее очереди. Функции не разрешается менять какую-либо память, кроме памяти под очередь.

  3. Вам дан исходный модуль queue.c для заголовочного файла queue.h из предыдущей задачи. Докажите полную корректность исходного модуля относительно вашей формальной спецификации из предыдущей задачи.

  4. Вам дан исходный модуль queue_prog.c для заголовочного файла queue.h и реализации очереди queue.c из предыдущей задачи. В этом модуле находятся функции, тестирующие очередь. Докажите полную корректность этого исходного модуля относительно вашей формальной спецификации очереди и реализации очереди.

  5. Разработайте реализацию очереди, выполняющую требования к queue.h. Эта реализация должна перевыделять память под buffer при ее недостатке в функции Queue__enqueue. Докажите полную корректность этой реализации. Докажите полную корректность queue_prog.c относительно вашей формальной спецификации очереди и новой реализации очереди.

  6. Вам дан заголовочный файл queue.h. Он содержит определения типов данных и заголовки функций для работы с очередями целых чисел. Ниже приведены требования к типу данных и функциям. Вам нужно формализовать эти требования в виде спецификации на языке ACSL и записать ее в заголовочном файле.

    Обратите внимание на то, что требования допускают множество реализаций. Внимательно отразите требования в формальной спецификации.

    Требования:

    Все функции возвращают 0 в случае успеха и ненулевое значение в случае неуспеха.

    Функция Queue__initialize инициализирует структуру данных queue пустой очередью. Если функция не может это сделать, она возвращает ненулевое значение.

    Функция Queue__finalize делает те действия, после которых нельзя считать, что в queue хранится какая-либо очередь. Если функция не может это сделать, она возвращает ненулевое значение.

    Функция Queue__enqueue вставляет в конец очереди значение item. Если функция не может это сделать, она возвращает ненулевое значение.

    Функция Queue__dequeue записывает по валидному указателю item элемент из начала очереди и удаляет его из очереди. Если функция не может это сделать, она возвращает ненулевое значение.

  7. Вам дан исходный модуль queue.c для заголовочного файла queue.h из предыдущей задачи. Докажите полную корректность исходного модуля относительно вашей формальной спецификации из предыдущей задачи.