我认为，在说俄语的互联网领域，形式验证的主题没有得到足够的涵盖，尤其缺乏简单明了的例子。
我将从国外获得这样的例子，并补充我自己的解决方案，以解决将狼，山羊和白菜运输到河对岸的众所周知的问题。
但首先，我将简要描述什么是形式验证以及为什么需要它。
形式验证通常意味着检查一个程序或算法是否使用另一个。
为了确保程序的行为符合预期，并确保其安全，这是必需的。
形式验证是发现和消除漏洞的最有效方法：它使您能够找到程序中所有现有的漏洞和错误，或证明它们不存在。
值得注意的是，在某些情况下这是不可能的，例如在8个皇后区且板宽为1000个单元的问题中：一切都取决于算法复杂性或停止问题。
但是，无论如何，都将收到三个答案之一：程序正确，不正确，或者无法计算答案。
如果找不到答案，通常可以对程序中晦涩难懂的地方进行修改，以降低其算法复杂度以获得特定答案（是或否）。
例如，在Windows内核和Darpa无人机操作系统中使用形式验证，以提供最大程度的保护。
我们将使用Z3Prover，这是一个非常强大的工具，用于自动证明定理和求解方程。
此外，Z3可以精确求解方程，并且不会用蛮力选择它们的值。
这意味着，即使在输入选项和10 ^ 100组合的情况下，他也能够找到答案。
但这仅是Integer类型的十几个输入参数，通常在实践中会发现。
8个皇后的问题（摘自英语
手册 ）。
# We know each queen must be in a different row. # So, we represent each queen by a single integer: the column position Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ] # Each queen is in a column {1, ... 8 } val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ] # At most one queen per column col_c = [ Distinct(Q) ] # Diagonal constraint diag_c = [ If(i == j, True, And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) for i in range(8) for j in range(i) ] solve(val_c + col_c + diag_c)
运行Z3，我们得到了解决方案：
[Q_5 = 1, Q_8 = 7, Q_3 = 8, Q_2 = 2, Q_6 = 3, Q_4 = 6, Q_7 = 5, Q_1 = 4]
皇后问题类似于一个程序，该程序接受8个皇后的坐标，并在皇后互相击败时显示答案。
如果我们要使用形式验证来解决这样的程序，那么与任务相比，我们只需要采取将程序代码转换为方程式的另一步骤即可：它实际上与我们的程序相同（当然，如果程序编写正确）。
搜索漏洞时几乎会发生同样的事情：我们仅设置所需的输出条件，例如admin密码，将源代码或反编译的代码转换为与验证兼容的方程式，然后我们得到答案，需要输入什么数据才能实现目标。
在我看来，狼，山羊和白菜的问题更加有趣，因为解决它已经需要许多（7）步骤。
如果皇后区的任务与您可以使用一个GET或POST请求穿透服务器的选项相当，那么狼，山羊和卷心菜就说明了一个例子，该例子来自更复杂和广泛的类别，在该类别中，只有几个请求可以到达。
例如，这与您需要查找SQL注入，通过它写入文件，然后增加权限并仅获得密码的情况相当。
问题条件及其解决方案农夫需要把狼，山羊和卷心菜运过河。 农民有一艘船，除了农民本人以外，只能放一个东西。 如果农夫无人看管，狼将吃山羊，山羊将吃白菜。
解决的办法是，在第4步中，农民将需要将山羊取回。
现在，让我们以编程方式启动解决方案。
我们将农夫，狼，山羊和白菜指定为4个变量，其值仅为0或1。零表示它们在左岸，而一表示在右岸。
import json from z3 import * s = Solver() Num= 8 Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ] Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ] Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ] Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ] # Each creature can be only on left (0) or right side (1) on every state HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ] WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ] GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ] CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ] Side = HumanSide+WolfSide+GoatSide+CabbageSide
Num是需要解决的步骤数。 每个步骤都是河流，船只和所有实体的状态。
现在，随机选择它，并取10个边距。
每个实体以10份副本表示-这是10个步骤中每个步骤的值。
现在我们设置开始和结束的条件。
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ] Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
然后，我们将狼吃山羊或山羊白菜的条件设置为公式中的限制。
（在农民面前，不可能进行侵略）
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
最后，我们询问农民在那里移动或返回时的所有可能动作。
他可以带狼，山羊或白菜，也可以不带，甚至不去任何地方。
当然，没有农民，没有人可以穿越。
这将通过以下事实来表示：河流，船只和实体的每个后续状态只能以严格受限的方式与先前的状态有所不同。
最多只能有2位，并且还有许多其他限制，因为农民一次只能运输一个实体，并且不能将所有实体放在一起。
Travel = [ Or( And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]), And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]), And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]), And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
运行解决方案。
solve(Side + Start + Finish + Safe + Travel)
我们得到了答案！
Z3找到了一组一致且令人满意的条件。
一种时空的多维转换。
让我们看看发生了什么。
我们看到，最终每个人都越过，直到开始时，我们的农民才决定放松身心，并且在前两个步骤中没有任何地方游泳。
Human_2 = 0 Human_3 = 0
这表明我们选择的州数量过多，而8个州就足够了。
在我们的案例中，农民这样做：开始，休息，休息，穿越山羊，向后穿越，穿过白菜，与山羊一起返回，穿越狼，独自返回，重新运送山羊。
但是最后，问题解决了。
#. Human_1 = 0 Wolf_1 = 0 Goat_1 = 0 Cabbage_1 = 0 # . Human_2 = 0 Wolf_2 = 0 Goat_2 = 0 Cabbage_2 = 0 # . Human_3 = 0 Wolf_3 = 0 Goat_3 = 0 Cabbage_3 = 0 # . Human_4 = 1 Wolf_4 = 0 Goat_4 = 1 Cabbage_4 = 0 # . Human_5 = 0 Wolf_5 = 0 Goat_5 = 1 Cabbage_5 = 0 # . Human_6 = 1 Wolf_6 = 0 Cabbage_6 = 1 Goat_6 = 1 # : . Human_7 = 0 Wolf_7 = 0 Goat_7 = 0 Cabbage_7 = 1 # , . Human_8 = 1 Wolf_8 = 1 Goat_8 = 0 Cabbage_8 = 1 # . Human_9 = 0 Wolf_9 = 1 Goat_9 = 0 Cabbage_9 = 1 # . Human_10 = 1 Wolf_10 = 1 Goat_10 = 1 Cabbage_10 = 1
现在，让我们尝试更改条件并证明没有解决方案。
为此，我们将给我们的狼赋予草食动物，而他将要吃白菜。
这可以与我们的目标是保护应用程序并且需要确保没有漏洞的情况相比。
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3给了我们以下答案：
no solution
这意味着确实没有解决方案。
因此，我们以编程方式证明了与杂食性狼穿越的可能性，而不会给农民造成损失。
如果读者发现这个话题很有趣，那么在以后的文章中，我将告诉您如何将普通程序或函数转换为与形式方法兼容的方程式并加以解决，从而揭示所有合法情况和漏洞。 首先，是在同一任务上，但是已经以程序的形式呈现出来，然后逐渐复杂化，并进入软件开发领域的相关示例。
以下文章已准备就绪：
从头开始创建正式的验证系统：我们用PHP和Python编写字符VM在其中，我从任务的正式验证到程序，再进行描述
如何将它们自动转换为正式的规则系统。