使用 Move 合约

Aptos CLI 主要用于编译,测试和形式化验证 Move 合约.如果你还没有安装 Aptos CLI,可以按照安装 Aptos CLI 的步骤进行安装.

你可以使用右侧的目录跳转到特定部分.

要了解如何使用 CLI 在链上链接 Move 合约,你可以按照这个”CLI 参数”教程进行操作.

你可以通过运行以下命令编译 Move 包:

aptos move compile --package-dir <你的包目录>

根据你的 Move.toml 文件中的设置,你可能需要向编译命令传递额外的信息.

例如,如果你查看 hello_blockchain 示例 Move 合约,在 Move.toml 文件中指定了一个名为 hello_blockchain 的地址变量.

[addresses]
hello_blockchain = "_"

因此,要编译它,你需要使用 --named-addresses 参数传入 hello_blockchain 的值. 你可以使用完整的地址,例如 0x123456...7890 或 CLI 中配置文件的名称,例如 default 或 superuser.

在我们的示例中,我们将使用 default:

aptos move compile --package-dir aptos-move/move-examples/hello_blockchain/ --named-addresses hello_blockchain=default

你可以通过运行 aptos move compile --help 了解编译 Move 合约时的可选参数.

…(about 300 lines omitted)…

对于需要保证代码按预期工作的情况(超出单元测试的范围),你可以使用 Move Prover 来形式化验证你的 Move 合约代码.

你可以按照这些步骤安装 Move Prover.

安装 Move Prover 后,你可以通过运行以下命令从 Aptos CLI 使用它:

aptos move prove --package-dir <你的包目录>

要了解如何形式化验证你的代码,请按照这里的深入 Move 教程进行操作(步骤 7 和 8 介绍了如何在示例代码中使用 Move Prover 和编写形式规范).