问题标签 [formal-methods]

我读过这个和这个。他们都无法帮助我解决这个问题。在此链接中，存储库中似乎没有任何内容，在此链接中，我按照它所说的每一步操作，但仍然无法为我的 Eclipse IDE获取CZT插件。

如何为 Eclipse IDE安装CZT插件？

注意：我的操作系统是 Ubuntu 16.04 LTS。似乎有一个 .exe 格式的 Eclipse IDE 版本已经启用了 CZT 插件。但由于我的操作系统不支持 .exe 文件，我无法通过这种方式解决此问题。

我将如何定义一个递归函数来找到比 VDM 中的输入数小二的最大幂？

功能如下：

最大：N -> N

到目前为止，我所拥有的是：

最大（n）=

if n=1 then 0
else if n=2 then 1
else ...最大（...）

我已经使用合金在模型中编写。但是，在某些情况下，运行谓词以查找实例失败，并且它表示找不到实例。我尝试将绑定增加到大约 16 个实例，但它没有找到任何实例。

有什么方法可以调试它，以便我可以看到哪些事实失败导致合金无法找到实例？

谢谢 ！

The ultimate in optimizing compilers would be one that searched among the space of programs for a program equivalent to the original but faster. This has been done in practice for very small basic blocks: https://en.wikipedia.org/wiki/Superoptimization

It sounds like the hard part is the exponential nature of the search space, but actually it's not; the hard part is, supposing you find what you're looking for, how do you prove that the new, faster program is really equivalent to the original?

Last time I looked into it, some progress had been made on proving certain properties of programs in certain contexts, particularly at a very small scale when you are talking about scalar variables or small fixed bit vectors, but not really on proving equivalence of programs at a larger scale when you are talking about complex data structures.

Has anyone figured out a way to do this yet, even 'modulo solving this NP-hard search problem that we don't know how to solve yet'?

Edit: Yes, we all know about the halting problem. It's defined in terms of the general case. Humans are an existence proof that this can be done for many practical cases of interest.

如何为对数组元素求和的函数编写 Spark 后置条件？（Spark 2014，但如果有人告诉我如何为早期的 Spark 做这件事，我应该能够适应它。）

所以如果我有：

在我的特定情况下，我不需要担心溢出（我知道初始化时的总数是多少，它只能单调减少）。

大概我在实现中需要一个循环变体来帮助证明者，但这应该是后置条件的直接变体，所以我还不担心。

我定义了 2 种几乎相同的语言（foo 和 bar）：

一个微不足道的语义：

打字：

我还定义了一个从 foo 到 bar 的翻译器：

我试图证明翻译器将 foo 表达式转换为具有相似类型的 bar 表达式：

并且转换还保留了表达式的语义：

我什至证明了一些归纳案例。但我无法证明FooToBar (FooVar x)案例的引理。

一般来说，不能证明 与FooVar x具有相似的类型或值BarVar x。

我想这FooToBar一定更复杂。它还必须涉及某种表达式环境或变量映射。你能推荐一个更好的签名FooToBar吗？我认为这样的翻译器是一件小事，但我找不到任何描述它的教科书。

考虑我在 B 规范中有以下内容：-

我是否可以创建如下改进：-

我有一个任务，它由 3 个并发的自定义（相互递归）进程组成。我需要以某种方式让它在计算机上执行，但是任何尝试将需求转换为程序代码的尝试都失败了，因为第一次迭代产生了 3^3 个实体和 27^2 个交叉关系，但它需要至少实现几次迭代尝试程序是否可以正常工作。

所以我决定放弃尝试理解整个系统并将问题形式化，现在想将其映射到硬件以生成算法并运行。语言无关紧要（甚至可能直接用于机器/组装？）。

我以前从未做过类似的事情，所以我搜索的所有主题，如算法综合、软硬件协同设计等，都提到硬件模型作为解决方案生成的后半部分（除了问题模型），但我从未见过. 整个作品应该是这样的：

我还不知道描述了什么级别的 硬件模型，所以无法决定必须如何将问题模型形式化以适应硬件模​​型层。
例如，目标系统可能包含 CPU 和 GPGPU，假设目标解决方案有 2 个并发进程。系统必须决定哪个进程在 CPU 上运行，哪个在 GPGPU 上运行。最高级别的解决方案可能来自将进程的计算强度与目标硬件进行比较，CPU 约为 300，GPGPU 约为 50。
但是一个正常的模型必须更完整，至少有缓存层次结构、内存访问批量大小等。
另一个例子是实现k-ary 树. k * i + c综合算法可以通过计算/( i - 1 ) / k 或存储直接指针来处理父母和孩子- 取决于computations per memory latency比率。

我在哪里可以获得要使用的硬件模型或数据？现在任何硬件都足够了——只是看看它的样子——以后获得现代处理器、GPGPU 和常见异构集群的模型会很棒。
制造商是否提供此类型号？描述他们的系统如何以任何形式语言工作。

假设我们试图形式化一些（半）群论性质，如下所示：

它工作得很好，但是，如果我们颠倒上述任何一个定义中的方程，即用

和

分别地，证明在 处失败reflexivity，因为其中一个或两个elim应用程序什么都不做。当然有一个解决方法，基于assert，但那是......太多的努力，只是烦人......

• 所涉及的 Coq 策略（ , 等）对顺序如此敏感，有什么原因elim吗case？我想，它不应该显着减慢战术（<< 2 次）。

• 有没有办法让它们symmetry在需要的地方自动应用，而不用每次都打扰我？在手册中找不到任何提及此问题的内容。

我有一个Array跟踪模式序列的Data模式。使用提升，我可以提升Increment操作以使用Array.

ArrayIncrement里面只增加一个数据Array。我怎样才能使它每增加一次 ？Data\ran data