问题标签 [kframework]

我正在使用 K 框架并尝试为类似于 ada-spark 的语言编写语义，并且在我声明一个整数变量本身时，我想编写涉及内存和值分配的语义。还

对于相同的方法，我尝试制作一个新单元格，但由于没有给出自定义配置的方法，因此我无法获得有用的结果。

我正在使用K 语义框架并运行教程，这是我的 TEST1.k ：

但是在运行命令 Komile Test1.k 时出现此错误：

我已经使用kompile foo.k.

但是，当我运行时，krun --directory foo-kompiled/ my-program.foo我看到以下错误：

如何正确使用此选项？

如何在我的语言中添加冒号作为句法结构？我已将它添加到语法中，但是当我尝试匹配规则中的冒号时，它会给我一个解析错误。

我正在尝试学习 kframework，作为练习，我想尝试创建一种高级语言，该语言可以编译为视频游戏的脚本语言。这种高级语言没有真正的执行，只是编译成带有重写规则的脚本语言。

下面的原始脚本语言语法示例

我希望我的高级语言允许正确的变量声明，所以我可以写这样的东西，它会编译成上面的脚本。

我知道如何制定一个简单的重写规则来用 替换变量声明var x = y，SetVariable("x", y)但我怎么还能附加到顶部的变量声明块？

我很可能误解了 K 的能力，或者我应该如何去做这件事。任何帮助，将不胜感激。

K教程中简要提到了上下文的使用，作为自定义订单评估的一种方式。但我也看到了其他包含重写箭头的上下文语句，比如无类型简单语言中的这个。

有人可以解释一下上下文在 K 中是如何工作的吗？我特别感兴趣的是：

• 在 K 中是否有context比仅说明评估顺序更普遍的用法？
• context声明语句的顺序如何影响语义？

谢谢！

我有以下 K 文件：

当我使用 Java 后端编译它并运行以下文件时：

我得到：

但我希望它代替Z并n得到Vector Z.

http://www.kframework.org/index.php/Lesson_4,_LAMBDA:_Generating_Documentation;_Latex_Attributes中的视频教程建议我们应该使用kompile lambda --pdf，但是当我运行它时出现以下错误：

该kdoc --help选项也会导致Command 'kdoc' not found错误。

如何正确使用此选项来生成格式化的 K 定义？

在修改教程中的玩具语言 SIMPLE 时，我认为有一个仅打印当前配置的语句会很有帮助，这样我就可以在程序运行时看到程序的内部状态。为此，我添加了Stmt一个printConfig命令。在语义上，我想我所要做的就是将其重写为调用单元格print的主体，T所以我添加了

编译器抛出一个错误，指出有一个意外的结束括号，特别是print(cfg). 我之前遇到过类似的问题，在这种情况下，错误原来是由于我输入的两个语句的组件造成的。我想知道是否有办法将T单元格中的值“转换”为 anExp以便我可以打印它。

如果有更好的方法可以调试不涉及此的语义，我也对此非常开放。谢谢！

例如，如果我有一些规则rule <k> foo bar => baz </k> <barList> bars </barList>并且我只想bar在列表中的时候加热规则，bars我相信我会添加requires bar in barsor when bar in bars。我一直使用when它作为我的首选，但阅读 K 手册待定文档似乎requires可能是首选。两者似乎都意味着“仅在满足此条件时才加热此规则”，因此我不清楚 和 之间的区别requires以及when在哪种情况下使用哪种情况。谢谢！