MOVE言語 チュートリアルStep_7 Move proveを使用する

どうもTABEです！
今回もチュートリアルやっていきます！

前回の記事

本家チュートリアル

Step_6とコードはほぼ同じため

新たに追加された部分だけ記載していきます。

move prover は形式検証ツールです。これを使うことで自動的に静的にプログラムをチェックすることができます

step_7では以下のソースコードが追加されています。

    spec balance_of {
        pragma aborts_if_is_strict;
    }

これを入れた状態で

move prove

を実行すると以下のエラーが出力されます。

ownerがリソースBalance<CoinType> を所有していないときに関数borrow_globalを呼び出すと発生するbalance_of関数がアボートする条件を明示的に指定する必要があると、proveaborts_ifr は基本的に告げているそうです。

このエラー情報を取り除くために、以下のようにaborts_if条件を追加します。(aborts_ifは公式の構文に載っていなかったのですが、条件に一致する時に処理を中止するものだと思われます。)

spec balance_of {
        pragma aborts_if_is_strict;
        aborts_if !exists<Balance<CoinType>>(owner);
    }

proveは正直よくわからなかったのですが
ドキュメントが充実していない状態なので
どんどん進めて実装することをよして進めようと思います！

やっとつぎのstep_8で最後ですが、一度やってみたのですが
ほぼ理解ができなかったので
他のチュートリアルを進めようと思います！

では、次回もよろしくお願いします！