正式方法被认为是确保软件可靠性的有效但不合理的复杂方法。 用于此目的的工具与程序员熟悉的工具有很大不同。 本文旨在降低进入此工具包的门槛。 我将使用
模型检查系统来解决软件规范中难以完成的任务，而是解决即使对于小学生而言也是可以理解的难题。
您位于一侧有七个房间的直接走廊中。 其中一只是猫。 第一步，您可以看看其中一个房间，如果有猫，他会被抓住。 门一关上，猫就会移入相邻房间中的另一间。 任务是抓猫。
TLA +和时间逻辑
有许多工具可以解决此类问题。 通常在这种情况下，使用
SMT求解器 。 通常，此类系统使用常规的谓词逻辑，并且表示操作序列非常复杂（您必须使用类似数组的东西，使用起来不太方便）。
TLA +使用时间逻辑，该逻辑允许在当前语句和下一步中的一条语句中使用系统状态。
CatDistr' = CatDistr \ {n}
此条件表明，在检查了房间n之后，可以将猫放置在其中的房间组与将猫移除n的房间组重合（如果猫在那里，他会被抓住，别无其他事情可做）。
在命令式编程语言中，这大致相当于为变量分配一个新值，该值是根据旧值计算得出的。
关于布景
如您所知，猫的位置是由变量模拟的，其中包含所有可能房间的集合，而不是特定房间的模拟，就像在模拟系统中一样。 在正式方法中，使用可能的值集而不是特定的值是一种经常使用的技术，这给新手程序员带来了困难。 因此，我选择了适合使用集合的任务。
TLA +中的程序结构
在最简单的情况下，程序由描述初始状态，当前状态与下一个状态之间的关系以及必须在所有可用状态中执行的不变式的声明和语句（谓词）组成。 辅助谓词也可能存在。 谓词可以参数化。
---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================
第一行和最后一行是模块声明的语法功能。
==表示“按定义等于”，而单个
=恰好等于表达式的计算值相等。
Doors是一个模型常数，需要在配置文件中进行设置。
CatDistr-猫在房间中的分布。
输入LastDoor变量（最后检查的房间）以提高程序输出的可读性。 对于大型模型，此类变量可以通过增加分析状态的数量来显着降低程序运行速度（因为状态现在包含其发生的历史，并且以不同方式创建的相同状态现在将有所不同）。
谓词Init描述初始状态（0..Doors是所有房间的集合）。 OpenDoor（n）描述了您打开房间n的门时发生的情况（在最坏的情况下，猫不在那儿-否则我们会抓住他）。
Next谓词看起来有些奇怪-有一个可供查看的空间。 事实是，某物的存在意味着TLA +不知道我们要进入哪个房间，因此，它将在所有情况下检查不变量的正确性。
写起来会更清楚
Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors)
但是我们的代码仅适用于固定数量的房间，最好对其进行参数化。
最后，CatWalk不变式是很多房间，其中猫可能不是空的。 违反不变式意味着无论原先在哪里猫都被抓住了。 在验证规格时，违反不变式意味着存在错误，但是我们并未将工具用于其预期目的，发现的“错误”意味着解决了问题。
型号配置
CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
这里的一切都很简单-我们指出了房间的数量，初始条件，状态改变的条件以及被测的不变性。
该模型是从命令行
tlc2 -config cat.cfg cat.tla启动的 。
TLA +具有由tla-toolbox团队启动的高级GUI。 不幸的是，他不了解.cfg文件，并且需要通过菜单配置模型参数。
结论
在此任务中，一切都变得非常简单。 当然，在实际中使用形式化方法的重大案例将需要更多的模型和各种语言结构的使用。 但是我希望解决此类难题将为在工作项目中实施形式化方法提供一种简单而不乏味的方法。
→在
这里找到任务
以防万一，一个用于
交互式解决方案验证的简单程序。
TLA +的
研究材料。
这里介绍
了另一个模型检查系统Alloy。