问题标签 [formal-verification]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
c - CCured在哪里下载？
在阅读了许多论文之后，我试图找到CCured源（甚至是二进制文件）来尝试在我的 C 源代码中使用它。
但是，所有链接似乎都已失效。经过一些谷歌搜索，我在这里问。如果您的硬盘上有一个压缩包，有人可以上传它们（来源、文档等）吗？
编辑：我还给其中一位作者发了电子邮件，但还没有得到回复。一段时间后将尝试给其他人发送电子邮件。
（引自论文）
CCured 一个程序转换系统，为现有的 C 程序添加类型安全保证。CCured 尝试静态验证内存错误不会发生，并在静态验证不足的地方插入运行时检查。CCured 通过根据使用情况分离指针类型扩展了 C 的类型系统，它使用了一种非常简单的类型推断算法，能够推断现有 C 程序的适当指针类型。CCured 使用物理子类型在编译时识别和验证大量类型转换。使用运行时类型信息验证其他类型转换。
formal-verification - 使用 Frama-C 验证 FFS（查找第一个集合）
我正在尝试验证 FFS 的软件实现。FFS 的作用是返回一个数字中最低位的索引位置（从 1 开始）。我尝试了许多不同的方式，包括使用幽灵变量。Jessie 无法验证，我不知道为什么？一些指示会非常有帮助。这是代码示例，我假设是 8 位数字：
proof - 有没有办法证明程序没有错误？
我在想我们可以证明一个程序有错误的事实。我们可以对其进行测试，以评估它或多或少具有抗虫性。
但是有没有办法（甚至理论上）证明一个程序没有错误？
对于简单的程序，比如“Hello World”，我想我们应该可以做到。但是更大的程序呢？
formal-verification - 如何解释 SPIN 错误输出？
我正在尝试对以下 LTL 属性的简单 Promela 模型进行模型检查：
我得到一个错误，错误线索上的引导模拟产生以下输出：
现在我看不到“M [0]直到M [1]”在这里被违反。M[0] 在初始化过程中被设置为 1，并且一直如此，直到 M[1] 变为 1。并且跟踪结束得这么早，或者我可能完全误解了“stronguntil”的语义。我非常有信心是这种情况......但我做错了什么？在 Promela 文件中指定 LTL 可以吗？
有问题的模型如下（一个简单的 petri 网）：
while-loop - 证明部分正确性的循环不变量
我试图找到一个循环不变量，以便我们可以证明这个程序部分正确：
我真的被困住了。到目前为止，我尝试过的一些不变量是：
和
我真的很感激一些建议。
if-statement - 如何将 if 语句添加到模式的后置条件？
我将为这个场景简化一些事情（它在 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在世界上最糟糕的工具中编译。
c# - C# 静态数组绑定检查
是否有 C# 工具可以静态（不执行代码）检测超出范围的数组访问，即会抛出IndexOutOfRangeException的数组访问。
谢谢你。
编辑：是的，我知道在一般情况下理论上是不可能做到的（即，它是不可判定的），但这并不意味着在某些情况下不可能做到（事实上整个领域形式验证是关于为理论上不可能的事情生产实用工具）。（我不认为这个表扬是特别需要的:)）
python - z3中一定大小的数组
我正在将 z3py 库用于程序验证项目，并希望对 z3 中数组的访问进行编码。有没有一种简单的方法可以使 Array z3type 具有一定的大小，例如 112 个条目？我在想类似的东西： A = Array('A', IntSort(), size)
谢谢，
z3 - 是否可以将一位的位向量转换为 SMTLib2 中的布尔变量？
我想要一个布尔变量来测试，例如，位向量的第三位是否为 0。位向量理论允许将 1 位提取为位向量，但不能提取布尔类型。我想知道我是否可以做这个演员。谢谢你。
=== 更新 ===
如果我的问题不清楚，我很抱歉。但 Nikolaj Bjorner 的答案是如何测试某个位向量的某个位。虽然我想将位向量的第一位的值分配给变量。我尝试将示例修改如下：
z3 抱怨：
我需要那个变量 bit0 供以后使用。你能给我一个提示吗？谢谢。