Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения

Д. Ю. Ковалев

?

Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения

С. 74–78.

В работе определен императивный язык программирования, учитывающий аппаратные ограничения вычислителя с набором инструкций RV32I, заданы его синтаксис и аксиоматическая семантика в виде логики Хоара. Необходимость подобного языка определяется невозможностью напрямую применять формальные доказательства, проведенные для программ на языках, не учитывающих аппаратные ограничения, к транслированному коду, исполняющемуся на реальном аппаратном вычислителе. В то же время, проведение доказательств для программ, написанных напрямую в кодах вычислителя, чрезвычайно трудоемко. Описанный язык учитывает такие аппаратные ограничения, как конечная ширина регистра, конечный объем памяти и использование арифметики по модулю вместо классической арифметики. В работе приведен пример программы вычисления НОД двух неотрицательных целых чисел, написанной на этом языке. Одним из направлений развития работы является построение алгоритма трансляции из определенного в работе языка в коды вычислителя и доказательство корректности этого алгоритма.

Язык: русский

Текст на другом сайте

Ключевые слова: формальные методы логика Хоара аксиоматическая семантика

В книге

Алгебра, теория чисел, дискретная геометрия и многомасштабное моделирование: современные проблемы, приложения и проблемы истории Материалы XXIII Международной конференции, посвящённой 80-летию профессора Александра Ивановича Галочкина и 75-летию профессора Владимира Григорьевича Чирского

Тула: Тульский государственный педагогический университет им. Л.Н. Толстого, 2024.

Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения

Ковалев Д. Ю., Чебышевский сборник 2025 Т. 26 № 3 С. 113–124

В статье определен императивный язык программирования, учитывающий аппаратные ограничения вычислителя с набором инструкций RV32I, заданы его синтаксис и аксиоматическая семантика в виде логики Хоара. Необходимость подобного языка определяется невозможностью напрямую применять формальные доказательства, проведенные для программ на языках, не учитывающих аппаратные ограничения, к транслированному коду, исполняющемуся на реальном аппаратном вычислителе. В то же время проведение ...

Добавлено: 5 ноября 2025 г.

Обзор применения формальных методов в робототехнике

Мордвинов Д. А., Литвинов Ю. В., Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление 2016 № 1 (236) С. 84–107

Представлен обзор применения формальных методов в контексте робототехники. Рассмотрены недавние работы, посвященные спецификациям поведения роботов в терминах темпоральных логик, применению идей подхода model checking к таким системам. также рассмотрено применение формальных методов анализа сетей Петри и моделирования поведения робототехнических систем с их помощью. Отдельное внимание уделено верификации гибридных систем, применению алгебр процессов для спецификации поведения ...

Добавлено: 30 октября 2018 г.

Анализ непротиворечивости моделей архитектуры предприятия с использованием формальных методов верификации

Бабкин Э. А., Пономарев Н. О., Бизнес-информатика 2017 Т. 43 № 3 С. 30–40

Разработка архитектуры предприятия является сложным процессом, но в то же время позволяет решить проблему синхронизации возможностей и потребностей бизнеса и информационных технологий (ИТ). Решение данной проблемы достигается за счет уточнения понимания и формализации описания бизнес-процессов и взаимодействия элементов системы путем их формального описания. Наличие большого числа взаимодействующих бизнес-процессов и сущностей архитектуры предприятия объясняет необходимость проверки ...

Добавлено: 3 октября 2018 г.

Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006.

Margaria T., Steffen B., IEEE Computer Society, 2006.

Добавлено: 30 сентября 2015 г.

Метод определения противоречий в DEMO-моделях бизнес-процессов

Бабкин Э. А., Бузуева А. А., Логвинова К. В., Бизнес-информатика 2014 № 2 С. 33–43

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

Добавлено: 17 апреля 2014 г.

Современные формализованные реконструкции Онтологического аргумента (на примере подхода Э. Залты и П. Оппенгеймера)

Пащенко Т. В., В кн.: Трансцендентное в современной философии: направления и методы.: СПб.: Алетейя, 2013.

Э. Залта и П. Оппенгеймер попытались создать свободное от модальных посылок прочтение рассуждения Ансельма Кентерберийского о существовании Бога, которое приводится во II главе Прослогиона. Несмотря на присутствие модальности в оригинальном тексте Ансельма (Нечто, более чего невозможно ничего помыслить), авторы обходят ее, заменяя процесс выведения актуальности Бога из возможности существования Бога на выведение существования Бога из ...

Добавлено: 18 февраля 2014 г.

Elections àla russe: formal establishment of rules and informal methods

Гельман В. Я., Osteuropa Zeitschrift für Gegenwartsfragen des Ostens 2005 Vol. 55 No. 10 P. 85–97

Добавлено: 24 ноября 2013 г.