В статье «Бесконфликтный реплицированный тип данных JSON» я встретил эту запись для формального определения «правил»:
Как называется эта запись? Как мне это прочитать?
Например:
DOC
правило не имеет ничего в своем «числитель» - почему?- то
EXEC
иGET
правила , по всей видимости, имеют два отдельных условия выше линии, что это значит? VAR
правило выделяется немного , как хорошо, так как в то время как многие другие правила используют какое - то стрелки (который я бы означать «подразумевает») наверху это один только кажется , говорят , что х есть элемент чего - то.- почти все приправлено инициалом,
Ap,
который в тексте описывается как «состояние реплики p описывается Ap, конечной частичной функцией» - как опытный читатель этой нотации будет «видеть» эту часть каждого правила?
На этом сайте был предложен связанный вопрос, который имеет очень похожую нотацию, на вопрос о значении ⟨B, s⟩ -> ⟨B ', s'⟩ как исходного правила в этом вопросе о малых шагах. семантика? - это помечено как операционная семантика , и это, кажется, является сильным лидерством. Действительно ли это та основа, в которой я должен интерпретировать эти цифры? Не могли бы вы вкратце изложить это в форме «ускоренного курса», чтобы, даже если я не смог проверить правильность их доказательств, я хотя бы смог немного лучше понять, что они говорят в этом разделе?
Вот очень неофициальное объяснение, которое может помочь людям, незнакомым с формальными обозначениями, войти в дверь. Это не заменяет формальное определение!
Ар является состоянием вашей системы или вашей работающей программы. «Состояние» может означать много вещей, но в этом случае оно включает список всех определенных локальных переменных и их значений. Почему Ap функция? Потому что это удобный способ выражения присваивания переменных: Ap (x) дает значение переменной x .
Теперь давайте возьмем правило EXEC в качестве примера. Он определяет семантику выполнения команды cmd1, за которой следует команда cmd2 , т. Е. Что происходит с состоянием Ap системы при выполнении cmd1, за которым следует cmd2 .
Другие правила описывают семантику отдельных команд и выражений. Например, правило VAR описывает, что значит «выполнять» переменную: если x - локальная переменная (над строкой), то что это значит для оценки / выполнения переменной x ? Это написано ниже строки: когда ваша программа находится в состоянии Ap , оценка x дает вам значение x , то есть Ap (x) .
Надеюсь, это поможет.
источник