问题标签 [kframework]

我正在学习语言 K，所以我开始用 K 实现一点 Pi-Calculus。我不明白为什么我的替换Q[Z/Y]在下面的程序中不起作用。

我的程序是：（(m(z) . m ! z) | (m ! 4 . m(x))两个线程之间的 ping/pong），并且使用下面的 K 语义，我得到了这个输出：

但z不能替代。我希望这个输出：

这是我对 Pi 演算的 K 语义。请注意，我使用x!y而不是x<y>发送构造。

先感谢您。

我想通过使用来自 KFramework 的 SIMPLE 的以下代码来实现多维列表

但是当我运行程序时它不能很好地工作：

显示 在这里输入图片描述 我发现它无法处理X[$1]，但是它知道如何处理X[4]，这意味着$1不能更改为4。我不知道原因以及如何处理。

如何使用 K Framework 转换以下 EBNF 规则？

一个元素可以用来表示前面的零个或多个：

现在，我正在使用Domain 模块中的 List 。但是内联List声明是不允许的，比如这个：

现在，我必须为列出的项目创建一个新的语法规则来解决这个问题：

是否有另一种方法来对抗这种新规则的创建？

一个元素可以出现零次或一次。换句话说，它可以是可选的：

我们要接受的地方：a[4]和a[]。现在，为了绕过这个，我创建了 2 条规则，其中一个分支有项目，另一个没有。但在我看来，这个解决方案以不必要的方式重复了规则。

一个元素可以出现以下一个或多个：

我们不接受任何非零长度的小写字母序列。现在，我没有找到模拟这个的方法。

先感谢您！

我正在定义Move IR的语法。该语言的测试套件包括各种注释以启用测试。我需要特别对待这种形式的评论：

该文件是一个示例algorithm_operators_u8.mvir。

到目前为止，我通过禁止普通的单行注释来实现这一点。

我也希望能够使用普通评论。作为第一步，我能够更改布局以仅在以!using开头时才允许提交r"(\\/\\/[^!][^\\n\\r]*)"

我想排除所有以评论开头//!或评论开头// check:的评论。什么是实现这一点的好方法？在哪里可以找到 K 使用的正则表达式语言的文档？

我正在尝试将表达式评估为值（Exps ::= Values）以进行函数调用。

这是一个简单的例子：

这被困在

.Exps ~> #freezer_(_) ERL-SYNTAX1 ( main )

所以我尝试了这条规则：.Exps => .Values 来评估 main()。

对我来说，奇怪的是，这次加热 3 是可以的：

.Values ~> #freezer_, ERL-SYNTAX1 ( 3 ) ~> #freezer ,_ ERL-SYNTAX1 ( 2 ) ~> ...

将会

3 , .Values ~> #freezer_,_ ERL-SYNTAX1 ( 2 ) ~> ..

但在这里它又卡住了。

我应该如何解决这个问题？

我正在尝试迁移使用该版本制作的语义：K tool, version 3.6 (yeah...)。我们有这个规则：

当我用 K 版本编译语义时：5.1.16和 LLVM 后端，我得到这个错误：

有没有办法支持这个版本的规则5.1.16？

当我尝试进行查找以获取存储在（常见模式）env配置中的变量的值时，我遇到了一个问题。Map以下是导致问题的语法和重写规则的提取代码：

当我运行一个小程序时，它卡在了这个配置中：

我希望这read(x)将在 中重写read(#loc(0))，但不应用该规则。如果我在规则中注释env配置要求并用 L常量替换0，则可以应用该规则：

我得到了终止.（因为其他规则将处理这个read(#loc(0))之后）

我还尝试在此处使用此文档中的此语法

但我得到一个解析错误

你有调试这个的想法吗？

我被困在一个功能的实现中，而且我不确定这是否是解决我的问题的正确方法。

我的问题描述

对于上下文，我希望能够borrow（一元操作）结构的字段，仅当该字段或其父字段上不存在引用时。让我用下面的例子来澄清我的这一点。我希望通过代码让事情变得更加清晰。

在这里，我有一个p包含嵌套字段和 3 个引用的结构：一个在 p 上，2 个在其字段上。

我使用 aMap来存储引用和它们之间的映射ref：

所以现在，如果我想在 p.p2.p3.x 上做一元运算符借用：

此操作应该失败，因为a,b and c存在于我的env.

我的代码

所以，我试图在这个片段中实现它：

我被困在如何实现该#checkborrow功能上。我的想法是首先生成给定路径的所有子路径，例如：

之后，做一个投影函数env来查看元素是否存在：

然后Set通过折叠OR #checkborrow({True, True, True, False}) => True减少返回值

目前，我被困在#pathToSubPath.

如果您有勇气阅读整个问题，谢谢您:)。我对K不熟悉，所以我正在寻求帮助。

注意： 我们使用的是这个版本的 K 框架：https ://github.com/kframework/k/releases/tag/nightly-f5ea5c7

我正在尝试安装 Kframework，但没有成功。我按照https://github.com/kframework/k/tree/master#prerequisite-install-guide上的说明安装了所有依赖项，并按照建议更新了环境变量。

我有 export PATH="~/z3-4.8.7-x64-osx-10.14.6/bin:$PATH" 。我正在运行：brew uninstall kframework brew uninstall z3，并卸载安装在 brew clean && brew update && brew upgrade brew install z3 kframework 之外的版本

Brew install kframework 产生以下有关命令行工具的警告： 警告：有较新的命令行工具版本可用。从系统偏好设置中的软件更新更新它们或运行：softwareupdate --all --install --force

如果没有显示任何更新，请运行： sudo rm -rf /Library/Developer/CommandLineTools sudo xcode-select --install

并最终以

<<< 错误！143 org.kframework.utils.errorsystem.KEMException：[错误]严重：无法启动z3进程（IOException：无法运行程序“z3”：错误= 2，没有这样的文件或目录）（即使我的CLT最多日期并安装在正确的位置）。

1. 我的 CommanLineTools 似乎是合法的。我有 Xcode 版本 11.3.1 (11C505)，并从我从苹果开发站点 Command_Line_Tools_for_Xcode_11.3.1.dmg 下载的二进制文件中安装了 CommanLineTools

键入“xcode-select -p”给出 /Library/Developer/CommandLineTools

2. 我的 z3 是：z3 -version Z3 版本 4.8.7 - 64 位（从 z3 网站下载的二进制文件）。

我也用 Z3 版本 4.8.12 试过这个

任何建议表示赞赏。

我对了解 K 前奏特别感兴趣（它的结构，为什么它的内容是这样的，“kompile”如何计算依赖关系等）。主要问题是：将 K 前奏曲中的钩子符号复制到生成的 Kore 文件中的标准是什么？

这里有一些潜在问题的例子：

1. 符号andBool与其关联的重写规则一起复制，符号in_keys似乎不是这种情况，它只是在没有重写规则的情况下复制。其他符号似乎是无用的（对于 IMP 语义），但在生成的 Kore 文件中存在，无论是否有其重写规则，例如countAllOccurrences、findChar、signExtendBitRangeInt或Float2String。

2. 似乎SortId是由 line 生成的syntax Id [token]。但是，线条"syntax Bool ::= "true" [token]并syntax Bool ::= "false" [token]不会生成真假符号。（此外，是否选择true和false是值而不是构造函数？）

3. 以下示例未生成名为SortId的排序，而一些生成的挂钩符号依赖于此排序。IMP 语义不存在这个问题。

4. 在每个后端的每种语言中都实现了 K prelude 是否正确，并且在 K prelude 中可以使用 Kore 语言的实现？你有必要的接口来实现一个新的后端吗？（例如，Bag是过时的，但不是Set，List和Map，但我不知道新后端必须提供的集合运算符、映射运算符等的列表。）

5. andThenBool和andBool一旦在 Kore 语法（布尔模块）中实现后具有相同的语义，有什么原因吗？

6. 为==Bool定义的重写规则在哪里，在=/=Bool（布尔模块）的定义中使用？