Mikino是一个（相对）简单的归纳和BMC引擎。它的目标是成为对形式验证感兴趣的人的一个简单而有趣的工具，特别是基于SMT的归纳。例如，mikino作为输入语言，比SMT-LIB 2（SMT求解器输入语言标准）更容易上手。我们还非常注重使其输出尽可能易于阅读和理解。

Mikino附带[关于SMT、归纳（和增强）的教程][dummies]。如果您对这两个主题中的任何一个都不熟悉，或者只是浏览一下整个示例，以了解mikino的滋味。

"Mikino" 并不意味着 cinema。它是 "mini" 和 "kinō"（帰納: induction, recursion）的缩写。它是现在已废弃的 kino k-induction引擎在转换系统上的一个显著简化版本。

内容

• 安装
• 基础知识
• SMT求解器（Z3）
• 从源码构建
• 转换系统
• 脚本
• 依赖项
• 许可证

安装

请确保Rust已安装并更新到最新版本。

> rustup update

使用cargo安装mikino。

> cargo install mikino

就这样。或者，您也可以从源码构建。

> mikino -V
mikino 0.9.0

基础知识

您可以使用mikino demo demo.mkn以演示模式运行mikino。这将写入一个带有大量注释的示例系统到demo.mkn中。下面有关于转换系统的讨论，详细介绍了输入格式，并以这个具体的系统为例。

运行mikino help也是一个好主意。

请注意，mikino文件被设计成与Rust语法高亮很好地协同工作。

SMT求解器（Z3）

Mikino需要一个SMT求解器来运行归纳（和BMC）。更确切地说，它需要一个Z3，您可以从Z3发布页面直接下载。您必须确保

• Z3二进制文件在您的路径中，并且称为z3，或者
• 使用 mikino 的 --z3_cmd 来指定如何调用它，例如
  • mikino --z3_cmd my_z3 ... 如果 my_z3 在您的路径中，或者
  • mikino --z3_cmd ./path/to/my_z3 ... 如果 path/to/my_z3 是 Z3 二进制文件的位置。

从源码构建

> cargo build --release
> ./target/release/mikino --version
mikino 0.9.0

转换系统

一个（转换）系统由一些变量声明组成，类型为 bool、int 或 rat（有理数）。这些变量的赋值通常被称为 状态。（这里的 int 是一个 数学 整数：它不会溢出或下溢。一个 rat 是 int 的分数。）

让我们用一个简单的计数器系统作为例子。假设这个系统有两个变量，cnt 类型为 int 和 inc 类型为 bool。

系统的定义具有一个 初始谓词。它是在系统变量上的布尔表达式，在系统的初始状态下评估为真。

假设我们希望允许计数器的 cnt 变量的初始值可以是任何正数。我们的初始谓词将是 cnt ≥ 0。请注意，变量 inc 在这个谓词中是不相关的。

接下来，系统的 转换关系 是两个变量版本的表达式：当前变量和下一个变量。转换关系是当前状态和下一个状态之间的关系，如果下一个状态是当前状态的合法后继，则评估为真。变量 v 的 下一个 版本写为 'v，而其 当前 版本简单地写为 v。

我们的计数器应该在变量 inc 为真时增加 1，否则保持其值。有几种方式可以编写它，例如

(inc ⋀ 'cnt = cnt + 1) ⋁ (¬inc ⋀ 'cnt = cnt)

或者

if inc { 'cnt = cnt + 1 } else { 'cnt = cnt }

或者

'cnt = if inc { cnt + 1 } else { cnt }

最后，转换系统有一个命名的候选者列表（候选不变式），它是变量上的布尔表达式。如果系统不通过重复应用转换关系从初始状态到达这些候选者的任何否定，则系统是 安全的。

计数器系统的合理候选者可能是 (≥ cnt 0)。对于这个候选者，系统是安全的，因为计数器可以到达的任何状态都不能否定它。

该候选者 ¬(cnt = 7) 在所有可达状态中并不成立，实际上初始状态 { cnt: 7, inc: _ } 也会使其不成立。但假设我们将初始谓词改为 cnt = 0。那么该候选者仍然可以通过将转换关系应用于（唯一的）初始状态 { cnt: 0, inc: _ } 七次来进行验证。在所有七次转换中，我们需要 inc 为真，以便 cnt 实际上增加。