代码之家 › 专栏 › 技术社区 › Dominykas Mostauskis

如何在TLA+中证明或模型检验定理?

tla+

0

Dominykas Mostauskis · 技术社区 · 7 年前

下面的模块声明一组介于10到99之间的数字,这些数字只能被2整除一次并调用它 NumbersThatDivideBy2Once input 是的子集 .

--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals

CONSTANT input

Numbers == { n \in Nat : n > 9 /\ n < 100 }

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

THEOREM input \subseteq NumbersThatDivideBy2Once

=======================

输入 ,即使其中一些数字不是我仍然没有错误。

1 回复 | 直到 7 年前

1

Jorge Adriano Branco Aires 7 年前

给你的定理起个名字,

THEOREM T == input \subseteq NumbersThatDivideBy2Once

转到“模型检查结果”选项卡,并在“计算常量表达式”中介绍 T ,以便对其进行评估。

您的模型检查器需要被告知如何处理规范文件,规范文件本质上只是数学定义的集合。

Spec 在规范文件中)。您可以在“模型概述”选项卡的“行为规范是什么?”下介绍它。这就是TLC用于执行模型检查的内容。

在这种情况下,你没有。因此,只需保留选项“no Behavior spec”,并如上所述,在“Model Checking Results”选项卡中指定要计算的常量表达式。