Операционная семантика операторов передачи управления в языке C на языке ABML

В работе рассматривается онтологический подход к заданию операционной семантики операторов передачи управления языка программирования C. В качестве формального средства используется предметно-ориентированный язык ABML, ранее предложенный для спецификации дискретных динамических систем, ориентированных на знания, структурированные в онтологиях. Показано, что операционную семантику фрагментов языков программирования, заданную в терминах систем переходов, можно интерпретировать как динамическую систему и формализовать средствами ABML. В статье вводится онтология операторов передачи управления языка C, включающая операторы goto, break, continue и return, а также онтологии конструкций, реагирующих на передачу управления, таких как помеченные операторы, блоки и оператор switch. Для этих онтологических моделей задается операционная семантика в виде атрибутных замыканий, вычисляемых относительно агентов и окружения. Особое внимание уделяется адаптации языка ABML к задачам задания операционной семантики, включая уточнение понятия атрибутного замыкания, введение стадий вычисления и явное моделирование контекста выполнения. Предложенный подход обеспечивает модульность, расширяемость и наглядность спецификации семантики. Полученные результаты демонстрируют применимость онтологического моделирования для формального описания семантики языков программирования и создают основу для дальнейшего расширения подхода на другие конструкции языка C, а также на анализ и верификацию программ.