问题标签 [formal-methods]

在我目前的项目中，我的老板分配了一项将领域特定语言的语法（用 ANTLR 编写）表达为正式语言/符号的工作。例如，以下是一小段语法代码。

据我所知，任何语言的 ANTLR 语法本身就是一个正式的规范。我不知道——我怎样才能指定这个语法是正式的方式。您能否给我一些将上述语法写入正式规范/数学符号的指示？

我有这个代码：

如您所见，taking是s映射到的关系的名称m。上面的关系显示了添加过程（联合），我在该关系中添加了一个新的 maptlet。

但是，我需要获取s此关系中可用的数量。我怎么才能得到它？以下是我所做的

但我不确定这一点。

我看到很多关于如何使用 ACL2 来证明代码的资源，正如您所期望的那样，但没有关于如何在生产中使用您的证明代码的资源。

我是否可以调整我的 ACL2 代码以使用 CLISP/Scheme/Clojure？ACL2 也可以运行我的代码吗？（教程在哪里，我使用 ACL2 不是按照它的目的吗？）

谢谢！

我将为这个场景简化一些事情（它在 Perfect Developer 中，它很快就会变得复杂）。假设我的类中有一个简单的模式，称为Succeed，它接受一个Course（这是一个先前定义的类）作为参数。

基本上，我想确保该课程set作为前提条件在我的课程中，然后将其添加到我coursesCompleted的后置条件中。这个简单的模式效果很好，看起来像这样：

但是，我想添加一个非常简单的if条件：如果我的 coursesCompleted 基数是 30 或更多，我想设置一个Diplomation枚举，比如说，“ Ok”。如果基数小于30，我将其设置为“ NotOk”

根据 Perfect Developer 的文档以及我见过的所有罕见示例，if语法应如下所示：

但是，如果我直接将其插入我的架构中，则如下所示：

它不起作用，我总是以“非常具有描述性”结束

错误！关键字“if”的语法错误，应为以下之一：“！” '(' '?' 'c_address_of'

我已经尝试;在任何地方添加一些，在 之后添加一个via关键字post，更改它的位置，;与 s交易,，以及许多其他反复试验的东西。

所以我的问题是：如何if在 Perfect Developer 中向模式的后置条件添加条件？

请在 Perfect Developer 中回答。我（遗憾地）知道我的正式方法，我只需要if在世界上最糟糕的工具中编译。

到目前为止，我已经为我的项目做了一点代码，但不知道它是真是假。你们能看到我的代码吗？首先，我应该发布要求以更好地理解..

在计算机科学中，互斥是指确保没有两个进程或线程同时处于其临界区的要求。临界区是指进程访问共享资源（如共享内存）的一段时间。互斥问题由 Edsger W. Dijkstra 于 1965 年在他的论文《并发编程控制问题的解决方案》中首次发现并解决。

有关问题的直观描述，请参见图。在链表中，节点的删除是通过将前一个节点的“下一个”指针更改为指向后续节点来完成的（例如，如果节点 i 正在被删除，那么节点 i-1 的“下一个”指针将是改为指向节点 i+1)。在多个进程之间共享这样一个链表的执行中，两个进程可能会尝试同时删除两个不同的节点，从而导致以下问题：设节点 i 和 i+1 为要删除的节点；此外，不要让他们成为头或尾；节点 i-1 的 next 指针将更改为指向节点 i+1，节点 i 的 next 指针将更改为指向节点 i+2。尽管两个删除操作都成功完成，节点 i+1 保留在列表中，因为 i-1 指向 i+1 跳过节点 i（该节点通过将下一个指针设置为 i+2 来反映 i+1 的删除）。可以使用互斥来避免此问题，以确保不会同时更新列表的同一部分。

这是我的代码：

我们有一个接受以下内容的操作 Bus_Arrives

一个 LINE、一个 BUS_ID 和一个 BUSROAD

• 给定线路的公共汽车到达车站并分配一条空的公共汽车路（如果有的话）。否则进入队列。

--------New_Bus_Arrives-------------------------------------------- -------------------------------------------------- ----

| Δ Bus_Station

| 公交线路？：LINE

| 总线？：BUS_ID

| br?: BUSROAD

===============================================

| 先决条件在这里（实现了将其添加到队列的情况，但我没有添加它，因为它与问题无关。）以下是此操作完成后系统如何更改。

| 免费' = 免费 \ {br?}

| 路由' = 路由

| 出发' = 出发 U {br? |--> 公交车？}

| 访问' = 访问 U {br? |--> 路由(|line?|) }

我的问题是：如果访问被正确表示为 Z，例如，当调用路由（线路？）关系时，它返回一组站元素 {station1，station2，station3}。但是，当我将其映射到访问关系以更新它时，我正在这样做：br？映射到 {station1,station2,station3}。这是可能的还是我不得不说这个？分别映射到集合的每个元素。此外，如果是这种情况，它如何在 Z 中表示？

关于所描述内容的额外信息：

路线：对于每条对应的公交线路，公交车经过哪些站点才能到达那里（即 - 8 号线前往洛杉矶、纽约和迈阿密）。

路由：LINE <--> STATION（关系）

免费：有哪些公交线路可用。

免费：Π BUSROAD（动力装置）

出发：对于每辆公共汽车它从哪条公交线路出发（例如从 A 出发的公共汽车 AY123）。

出发：LINE --> BUS_ID（函数）

访问：对于当前分配了公共汽车的每条公共汽车道路，它将访问哪些站点。一条公共汽车路可以有一辆且只有一辆公共汽车，也可以是可用的。

访问：BUS_ROAD <--> STATION（关系）

我想知道是否可以在event-b中仅使用一个lambda表达式生成一系列素数。这是我到目前为止所拥有的：

@axm1生成一组素数，@axm2定义序列的类型并将@axm3该集合进一步约束为确定性解决方案。我不知道如何用一个 lambda 表达式来做到这一点，我认为这甚至不可能，但我想知道其他人的想法。

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？以下算法找到最大值是否正确？

答案必须基于算法最弱前提的计算。

你如何验证这一点？似乎很简单。

谢谢。

我想用 Python 编写一个可扩展的程序，该程序将根据用户输入创建合金模型。特别是，我希望用户输入一个图形并使用 Alloy 告诉用户该图形是否具有欧拉路径。我已经在 Alloy 中为特定的图形实例准备好了模型。但是，我正在考虑通过 Python 代码生成 .als 文件，然后通过 Python 启动 Alloy 来评估模型。是否有我可以使用的 Alloy API 或任何命令行参数可以帮助我确定某个谓词是否一致？

谢谢

有没有办法在合金中使用袋子（多组）对系统进行建模？如果没有明确的袋子概念，是否有任何可能的解决方法？

谢谢。