Очередное заседание семинара:

24 апреля 2018 года в 18:25

(Главное здание МГУ имени М. В. Ломоносова, аудитория 1408)

Кривчиков М. А. (МГУ имени М.В. Ломоносова)
«Описание семантики предметно-ориентированных языков программирования с использованием подтипов»

Аннотация доклада.

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