时间戳

首页 > 解决方案 > 如何理解伊莎贝尔的语法和翻译

syntax - 如何理解伊莎贝尔的语法和翻译

问题描述

我正在尝试理解 Isabelle/HOL 中的 Rely Guarantee 代码，并对https://isabelle.in.tum.de/library/HOL/HOL-Hoare_Parallel/RG_Syntax.htmlsyntax中的andtranslation关键字 感到困惑

syntax
  "_Assign"    :: "idt ⇒ 'b ⇒ 'a com"                     ("(´_ :=/ _)" [70, 65] 61)
  "_Cond"      :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
  "_Cond2"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
  "_While"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
  "_Await"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0AWAIT _ /THEN /_ /END)"  [0,0] 61)
  "_Atom"      :: "'a com ⇒ 'a com"                        ("(⟨_⟩)" 61)
  "_Wait"      :: "'a bexp ⇒ 'a com"                       ("(0WAIT _ END)" 61)
  "_PAR"       :: "prgs ⇒ 'a"                              ("COBEGIN//_//COEND" 60)

我对三个问题感到困惑

(1) 为什么名字前总有下划线_Assign？

(2) 斜线、单引号(´_ :=/ _)和双斜线是什么意思COBEGIN//_//COEND

（3）为什么mixfix符号前有一个零0IF _ THEN _ FI

translations
  "´x := a" ⇀ "CONST Basic «´(_update_name x (λ_. a))»"
  "IF b THEN c1 ELSE c2 FI" ⇀ "CONST Cond ⦃b⦄ c1 c2"
  "IF b THEN c FI" ⇌ "IF b THEN c ELSE SKIP FI"
  "WHILE b DO c OD" ⇀ "CONST While ⦃b⦄ c"
  "AWAIT b THEN c END" ⇌ "CONST Await ⦃b⦄ c"
  "⟨c⟩" ⇌ "AWAIT CONST True THEN c END"
  "WAIT b END" ⇌ "AWAIT b THEN SKIP END"

print_translation ‹
  let
    fun quote_tr' f (t :: ts) =
          Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>‹_antiquote› t, ts)
      | quote_tr' _ _ = raise Match;

    val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>‹_Assert›);

    fun bexp_tr' name ((Const (\<^const_syntax>‹Collect›, _) $ t) :: ts) =
          quote_tr' (Syntax.const name) (t :: ts)
      | bexp_tr' _ _ = raise Match;

    fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
          quote_tr' (Syntax.const \<^syntax_const>‹_Assign› $ Syntax_Trans.update_name_tr' f)
            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
      | assign_tr' _ = raise Match;
  in
   [(\<^const_syntax>‹Collect›, K assert_tr'),
    (\<^const_syntax>‹Basic›, K assign_tr'),
    (\<^const_syntax>‹Cond›, K (bexp_tr' \<^syntax_const>‹_Cond›)),
    (\<^const_syntax>‹While›, K (bexp_tr' \<^syntax_const>‹_While›))]
  end
›

而且我无法理解上面代码的含义。我在哪里可以找到有关使用translations和的参考print_translation

标签： syntaxverificationisabelleformal-verificationformal-methods

解决方案

您可以在 Isabelle 的标准参考手册（Isar-ref 或Makarius Wenzel的 The Isabelle/Isar Reference Manual ）的第 8 章中找到您要查找的信息。更具体地说，请参阅参考手册中的第 8.2、8.4 和 8.5 小节。

就我个人而言，我不熟悉 Isabelle 中语法转换的实现细节，所以我的答案将依赖于文档中已经说明的内容。因此，我的建议是使用参考手册作为主要信息来源。如果在阅读了参考手册后，您还有其他问题，不妨试试 Isabelle 或 Zulip chat 的邮件列表。

  1. 该命令syntax在参考手册的 8.5.2 小节中进行了解释。在您的问题中，_Assign是语法声明的语法常量，它只是 Isar 语言的语法实体中的一个名称（参见参考手册中的第 3.2 小节）。从技术上讲，下划线应该没有特殊含义，但是在语法常量名称的开头使用下划线是一种约定，似乎只有语法常量的名称可以以下划线开头。
  2. 参考手册中的第 8.2 小节已经包含对您的第二个问题的相当详细的答案。´mixfix 模板中的单引号(´_ :=/ _)没有任何特殊含义。但是，/允许（但不强制）换行并//在漂亮打印期间强制换行。
  3. 一般来说，(n作为n一个自然数，在 mixfix 注释中打开一个漂亮的打印块。数字n指定块缩进（即，在块中出现换行时添加的空格数）。但是，如果n未指定，则应默认为0. 所以，我不完全确定为什么0在这种情况下确实需要。您可能希望进一步调查。

命令translations和print_translation分别在 8.5.2 和 8.5.3 小节中解释。因此，translations可用于指定 AST 的重写规则，同时print_translations允许对打印的内部语法进行任意操作（请记住粗略的“术语->AST->漂亮打印文本”序列）。在这种情况下，您可以直接检查调用的效果，print_translation如下所示

lemma "´a := b = c"
  (*Basic (a_update (λ_. b)) = c*)
  oops

print_translation ‹…›

lemma "´a := b = c"
  (*´a := b = c*)
  oops

希望这会有所帮助，或者至少可以为您指明相关资源的方向。

推荐阅读