其他
Move硬核研究系列 | 智能合约的重要变革，如何使用Move Prover？
#安装
git clone [https://github.com/move-language/move.git](https://github.com/move-language/move.git)cd move && ./scripts/dev_setup.sh -yptmove prove -t TEST_NAME#应用场景
1 权限控制
在规范层面上强制执行明确的访问控制策略可以有效防止权限滥用。
例如，在std::offer中，我们可以看到，当接收者不在白名单中，该函数会被终止。
spec redeem { ... aborts_if !is_allowed_recipient<Offered>(offer_address, signer::address_of(account)); ... }struct Account has key { balance: u64}
const MAX_BALANCE: u64 = 1000;
fun deposit(target: address, amount: u64) acquires Account { let account = borrow_global_mut<Account>(target); let new_balance = account.balance + amount; assert!(new_balance <= MAX_BALANCE, 0); account.balance = new_balance;}invariant forall a: address where exists<Account>(a): balance(a) <= MAX_BALANCE;public fun swap<X, Y, Curve>( x_in: Coin<X>, y_in: Coin<Y>, ): (Coin<X>, Coin<Y>) acquires Pool { ...
let x_reserve_size = coin::value(&pool.coin_x_reserve); let y_reserve_size = coin::value(&pool.coin_y_reserve);
// Deposit new coins to Pool. coin::merge(&mut pool.coin_x_reserve, x_in); coin::merge(&mut pool.coin_y_reserve, y_in);
spec { coin::value(&pool.coin_x_reserve) > x_reserve_size || coin::value(&pool.coin_y_reserve) > y_reserve_size; };
... }