米科诺是一个（相对）简单的归纳和BMC引擎。它的目标是作为一个简单但有趣的工具，供那些对形式化验证，尤其是基于SMT的归纳感兴趣的人使用。例如，与SMT-LIB 2（SMT求解器输入语言标准）相比，mikino 作为输入语言要容易得多。我们还非常注重使其输出尽可能易于阅读和理解。

米科诺附带 [SMT、归纳（和强化）教程][dummies]。如果您是这两个主题的新手，或者只是想看看示例，以了解米科诺的用法，请务必阅读。

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

Contents

• 安装
• Basics
• SMT Solver (Z3)
• Building From Source
• Make sure Rust is installed and up to date.
• Use cargo to install mikino.
• Use cargo to install mikino.
• Use cargo to install mikino.

安装

Use cargo to install mikino.

> rustup update

Use cargo to install mikino.

> cargo install mikino

Use cargo to install mikino.

> mikino -V
mikino 0.9.0

Basics

Use cargo to install mikino.

Use cargo to install mikino.

Use cargo to install mikino.

SMT Solver (Z3)

Use cargo to install mikino.

• Use cargo to install mikino.
• 使用 mikino 的 --z3_cmd 指定如何调用它，例如
  • mikino --z3_cmd my_z3 ... 如果 my_z3 在您的路径中，或者
  • mikino --z3_cmd ./path/to/my_z3 ... 如果 path/to/my_z3 是 Z3 二进制文件所在的位置。

Building From Source

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

Make sure Rust is installed and up to date.

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

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

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

假设我们希望允许计数器的 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 的值。

候选者的反例是一个 具体轨迹：一个从初始状态开始的连续状态序列 i)，其中后续状态通过转换关系有效，ii) 且序列的最后一个状态反例化了 PO。

对于上述最后一个系统，使用修改后的初始谓词，¬(cnt = 7) 的反例是

Step 0
| cnt: 0
Step 1
| cnt: 1
| inc: true
Step 2
| cnt: 2
| inc: true
Step 3
| cnt: 3
| inc: true
Step 4
| cnt: 4
| inc: true
Step 5
| cnt: 5
| inc: true
Step 6
| cnt: 6
| inc: true
Step 7
| cnt: 7
| inc: true