Практическое задание

map.h

В этом задании вам нужно написать спецификацию на языке ACSL для данных структур данных и только для данных вам в задании функций. Помимо этого, вам необходимо продемонстрировать полноту спецификации в обе стороны (то есть, что любая программа, удовлетворяющая вашей спецификации, будет удовлетворять этим требованиям, и наоборот). Это можно сделать трассировкой (установлением соответствия) частей требований на части спецификации и в обратную сторону (то есть спецификация содержит все требования и не утверждает того, что не утверждают требования). Можно показать полноту спецификации и иначе: составить и реализовать тестовые сценарии с их дальнейшей верификацией при помощи связки инструментов, причем тестовые сценарии должны тоже полностью покрывать все требования, но не включать тех сценариев, которых нет в требованиях.

Вам дано определение структуры данных Map для хранения отображений элементов типа Key в элементы типа Value (ассоциативный массив). Структура может хранить лишь единственное отображение для конкретного
ключа.

typedef struct {
    int a;
    int b;
} Key;

typedef struct {
    int c;
    int d;
} Value;

typedef struct {
    Key key __attribute__((noembed));
    Value value;
    int existent;
} Item;

typedef struct {
    Item *items;
    int capacity;
    int count;
} Map;

Поле items структуры Map представляет собой массив длины capacity. Поле count этой структуры определяет, сколько элементов данного массива имеет поле existent установленным в истину (единицу). При работе со структурой учитываются те и только те записи массива items, которые имеют булево поле existent установленным в истину (единицу).

Никакие операции над структурой данных не должны приводить ее в такое состояние, чтобы после этого добавление одного отображения увеличило количество отображений более, чем на 1. Это делается для того, чтобы была возможна эффективная реализация операции добавления отображения.

Вариант А: Отображения хранятся как последовательность пар ключ-значение в массиве items, возможно с некоторыми пропусками между ними (у пропусков поле existent установлено в ложь). Элементы хранятся с начала массива. При этом считается, что за двумя последовательно идущими элементами, у которых existent установлен в ложь, остальные элементы тоже имеют existent установленным в ложь.

Вариант B: Отображения хранятся в хэш-таблице, представленной массивом items. Используется хэш-функция hash(). Используется линейное пробирование, то есть для доступа к информации о паре для заданного ключа key поиск начинается c элемента массива items по индексу hash(key) % capacity и идёт последовательным увеличением индекса на единицу по модулю capacity. Если очередной элемент имеет поле existent установленным в ложь или пройден полный круг, а элемент соответствующий заданному key ключу не встречен, то считается, что такой ключ не содержится в данном ассоциативном массиве.
Определение hash: logic integer hash{L}(Key *k) = k->a * 33 + k->b;

Функция createMap() создаёт и возвращает пустой ассоциативный массив с заданным числом максимально хранимых элементов size, выделяя под него динамическую память; в случае неуспеха, функция должна вернуть нулевой указатель.
Сигнатура функции: Map *createMap(int size);

Функция deleteMap() освобождает память, занимаемую ассоциативным массивом map. На вход функции должен подаваться указатель на освобождаемую область памяти.
Сигнатура функции: void deleteMap(Map *map);

Функция addElement() добавляет в заданный ассоциативный массив map отображение заданного ключа key на заданное значение value и возвращает истину (единицу), если в нём было место для этого отображения. Если в ассоциативном массиве было недостаточно места, функция возвращает ложь (ноль). Функция не меняет переданные ключ и значение. Функция имеет право изменять структуру ассоциативного массива, если это не отражается на содержащихся в нём парах. Ничего другого функция не делает.
Сигнатура функции: int addElement(Map *map, Key *key, Value *value);

Функция removeElement() удаляет сохранённое в ассоциативном массиве map значение по заданному ключу key (если оно там было). Функция не удаляет другие отображения, кроме отображения по заданному ключу, а также не добавляет новые отображения. Функция возвращает истину (единицу), если функция изменила ассоциативный массив, ложь (ноль) в противном случае. В случае, если значение было удалено и при этом переданный указатель value был отличен от нулевого, функция записывает значение, содержавшееся для заданного ключа, по данному указателю. Функция имеет право изменять структуру ассоциативного массива, если это не отражается на содержащихся в нём парах. Ничего другого функция не делает.
Сигнатура: int removeElement(Map *map, Key *key, Value *value);

Функция getElement() возвращает по указателю value сохранённое в ассоциативном массиве map значение для заданного ключа key и возвращает истину (единицу), если заданный ассоциативный массив имеет отображения для заданного ключа. В случае, если значение по заданному ключу не содержится в отображении, возвращается ложь (ноль) и ничего другого не происходит. Функция не меняет ассоциативный массив и переданный ключ. Ничего другого функция не делает.
Сигнатура функции: int getElement(Map *map, Key *key, Value *value);