Исполняемая спецификация..? Как исполняемые спецификации могут быть использованы для быстрого прототипирования?

Question

После прочтения этих книг

Бертран Мейер, Введение в теорию языков программирования и

Дж. Д. Ульман, Элементы программирования ML

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

У меня есть несколько вопросов... Я не понимаю значения некоторых строк, и у меня также есть некоторые вопросы... что это значит и что такое "исполняемая спецификация"

(1) семантическая спецификация исполняемого языка в SML как быстрый прототип языковой реализации

(2) как исполняемые спецификации могут быть использованы для быстрого прототипирования

(3) Денотационная семантика обеспечивает "оракула" реализации императивных языков программирования на доступных архитектурах / машинах.

Answer 1

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

datatype value = Int of int
               | String of string

datatype ast = Seq of ast * ast
             | Print of ast
             | Value of value
             | Assign of string * ast
             | Variable of string

fun value_printer (Int i) = print (Int.toString i)
  | value_printer (String s) = print s

fun execute env (Seq (a, b)) = (execute env a; execute env b)
  | execute env (Print a) = value_printer (execute env a)
  | execute env (Value _) = ()
  | execute env (Assign (s, a)) = ...
    etc, etc.

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

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

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