首页 文章

Alloy 4,Software Abstractions 2E和seq关键字

提问于
浏览
1

不久前我获得了第二版的软件抽象,当我需要刷新我的记忆如何拼写 elems 函数的名称时,我想"Oh, good, I can check the new edition instead of trying to read my illegible handwritten notes in the end-papers of the first edition."

但我找不到"seq"或"elems"或索引中任何其他辅助函数的名称,也没有在附录B的语言参考中看到 seq 关键字的任何提及 .

似乎可能出现以下一种或多种情况;哪一个?

  • 我错过了什么 . (什么哪里?)

  • 附录B中未涵盖 seq 关键字,因为严格来说, set 和其他一元运算符的关键字并不严格 . (请解释!)

  • 在第二版出版后,对Alloy 4的序列支持已经添加,因此需要通过参考网站上Quick GuideAlloy 4 grammar中Alloy 4中新功能的讨论来增加该书 . (啊,好的 . 页面很慢,位很快 . )

  • 其他......

我想,试图在这里提出一个普遍有用的问题,我在问:Alloy Analyzer 4.2(或任何4. *)实现的语言与软件抽象第二版中定义的语言之间的关系究竟是什么?

1 回答

  • 3

    当前实现对应于this在线文档 .

    序列实际上不是语言的一部分; x: seq A 可以看作是 x: Int -> A 的语法糖,并且所有效用函数(例如, firstlastelems )都是库定义的(在 util/sequence 中) . 实际的实现有点复杂(只是为了让我们可以让用户编写像 x.elems 之类的东西并同时让类型检查器开心),但从概念上讲,这仍然是_1294014 .

相关问题