第7节：使用prover

首先安装：

./scripts/dev_setup.sh -yp
Y
cargo build
source ~/.profile

Move prover

Code

在上一节的BasicCoin中增加如下代码：

    spec balance_of {
        pragma aborts_if_is_strict;
    }

执行：

move prove

报错：

修改代码：

    spec balance_of {
        pragma aborts_if_is_strict;

          // 增加这行代码
        aborts_if !exists<Balance<CoinType>>(owner);
    }

重新运行：

move prove

结果如下：

Note