符号测试

本文详细介绍了形式化验证（formal verification）的过程及其在智能合约中的应用，强调了与单元测试的互补关系，以及如何利用Halmos工具简化形式化验证的实施。文中分析了正式验证的挑战、规范的编写开销及其在ERC721A智能合约中的案例，展示了通过符号测试实现高效验证的重要性。

本文介绍了如何使用 Halmos 编写符号测试，符号测试与模糊测试类似但存在差异。文章详细讲解了编写符号测试的步骤，包括安装 Halmos、编写 setUp() 函数初始化合约状态、以及编写具体的符号测试，其中涵盖了声明符号输入、设定输入条件、调用目标合约以及检查输出状态，并强调了符号测试中需要注意的细节和与模糊测试的区别，例如使用 vm.assume() 替代 bound() 等。