Верификация объектно-ориентированных программ с динамической памятью на основе ссылочной модели
Предложен метод аксиоматичной верификации динамической памяти на основе логического языка программирования "Пролог" для объектно-ориентированных программ, использующих ссылочную модель памяти. Формально определены термины: куча, интерпретация кучи и рассмотрены формальные операции над кучами. Обобщенная реализация на Прологе разрешает преодолевать недостатки в выразимости. Сделаны предположения, что представленным подходом можно решить совокупность других актуальных проблем в той же области. Предполагаемая модель была проверена с помощью системы верификации, которая, в том числе, способна преобразовывать программы императивных языков с экземплярами классов в промежуточное представление.
Авторы: Р. Хаберланд, С. А. Ивановский, К. В. Кринкин
Направление: Информатика и компьютерные технологии
Ключевые слова: Указатели, кучи, анализ псевдонимов, верификация динамической памяти
Открыть полный текст статьи