编写一个计算机程序来分析另一个计算机程序的质量？答案

【问题标题】：Writing a computer program that will analyse the quality of another computer program?编写一个计算机程序来分析另一个计算机程序的质量？
【发布时间】：2019-03-31 10:40:19
【问题描述】：

我有兴趣了解这种可能性。我正在开展一个验证软件工程师技能的项目，目前我们根据有资质的开发人员的代码审查来验证技能。

如果比这个问题更完整，我知道答案，我无法想象程序必须能够分析复杂的代码有多复杂，但我从基本的编程面试问题开始。

例如经典的 FizzBuzz 问题：

编写一个打印从 1 到 20 的数字的程序。但是对于 3 的倍数打印“Fizz”而不是数字，对于 5 的倍数打印“Buzz”。对于同时是 3 和 5 的倍数的数字，打印“FizzBuzz”。

以下是python中的解决方案：

for num in range(1,21):
    string = ""
    if num % 3 == 0:
        string = string + "Fizz"
    if num % 5 == 0:
        string = string + "Buzz"
    if num % 5 != 0 and num % 3 != 0:
        string = string + str(num)
    print(string)

问题是，我们能否以编程方式分析此解决方案的有效性？

我想知道是否有人尝试过这个，如果有当前的实现，我可以看看。另外，如果有人用过 z3，如果它是我可以用来解决这个问题的东西。

【问题讨论】：

标签： testing automated-tests z3 software-quality

【解决方案1】：

正如 Vilx 所提到的，程序的正确性（包括它们是否终止）通常是不可判定的。然而，Z3 等工具表明，尽管问题普遍具有不确定性，但相关的具体案例仍然可以推理。

静态分析器通常会寻找“简单”的问题（例如空值取消引用、越界访问、数值溢出），但速度相对较快，并且几乎不需要用户指导（想想在代码中添加类型注释的精神）。

要搜索的关键字的非详尽（且有偏见）列表：“静态分析器”、“抽象解释”； “facebook infer”、“airbus absint”、“juliasoft”。

验证器试图证明更丰富的属性，特别是功能正确性，例如“这种排序实现是否真的对我的数组进行了排序（而不做任何其他事情，例如释放一些全局内存或更新数组中可访问的元素）？”或“该加密实现真的实现了它承诺实现的加密协议吗？”。这是一项非常艰巨的任务，并且该研究领域的工具通常相当缓慢，需要具有形式验证背景的专家用户和重要的用户指导。

要搜索的关键字的非详尽（且有偏见）列表：“验证”、“霍尔逻辑”、“分离逻辑”； “eth viper”、“microsoft dafny”、“kuleuven verifast”、“microsoft f*”。

存在其他正式方法，例如细化（或按构造修正），但工具支持更少，据我所知，行业接受度更低。

【讨论】：

【解决方案2】：

让我们这样说吧：数学证明您不能确定如果程序将永远终止。所以，如果你想得到一个数学上完美的答案来判断目标程序是否正确，那你就完蛋了。

也就是说，您仍然可以进行单元测试和“linting”，这将为您提供大量有趣的见解。

但是对于像 FizzBuzz 这样的简单代码，我认为由经验丰富的开发人员进行观察可能会带来最好的结果。

【讨论】：