[More Detail] [Collapse All]
Feature: Withdraw pattern of sending Ether


The recommended method of sending funds after an effect is using the
withdrawal  pattern in [http://solidity.readthedocs.io/en/develop/common-patterns.html].

This is an example of the withdrawal pattern in practice in a
contract where the goal is to send the most money to the contract in
order to become the “richest”, inspired by King of the Ether.
features/050-ether-balance/250-withdraw-pattern.feature
- Background: Create 'WithdrawalContract' and define setups
link
features/050-ether-balance/250-withdraw-pattern.feature:11
Given I create initial sbuilder context with:
Directory
solidity WithdrawalContract
setup setup1
And a file named "solidity/WithdrawalContract.sol" with:

   pragma solidity ^0.4.0;

   contract WithdrawalContract {
       address public richest;
       uint public mostSent;

       mapping (address => uint) pendingWithdrawals;

       function WithdrawalContract() payable {
           richest = msg.sender;
           mostSent = msg.value;
       }

       function becomeRichest() payable returns (bool) {
           if (msg.value > mostSent) {
               pendingWithdrawals[richest] += msg.value;
               richest = msg.sender;
               mostSent = msg.value;
               return true;
           } else {
               return false;
           }
       }

       function withdraw() returns (bool) {
           uint amount = pendingWithdrawals[msg.sender];
           // Remember to zero the pending refund before
           // sending to prevent re-entrancy attacks
           pendingWithdrawals[msg.sender] = 0;
           if (msg.sender.send(amount)) {
               return true;
           } else {
               pendingWithdrawals[msg.sender] = amount;
               return false;
           }
       }
   }
- Scenario: Create contract, mine and send ether
link

See the comments in the setup for explanation

State space

    Steps exuted:

    step 5 - WithdrawalContract() --> p_WithdrawalContract__
    step 6 - WithdrawalContract(becomeRichest) --> p_WithdrawalContract_becomeRichest_
    step 7 - WithdrawalContract(withdraw)  -> p_WithdrawalContract_withdraw_


     Account balances:
                acc1   acc2   acc3
     Step 2:       5      -     - 
     Step 4:       5      3     - 
     Step 5:       4      3     1
     Step 6:       4      0     4
     Step 7:       7      0     1
     

     Richest && mostSent
     
               richest      mostSent
     State 5:     acc1            1
     State 6:     acc2            3
     State 7:     acc2            3

     pendingWithdrawals:
                acc1    acc2     acc3
     State 5:    0       0        0 
     State 6:    3       0        0 
     State 6:    0       0        0
features/050-ether-balance/250-withdraw-pattern.feature:60
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:


     - domain: eth_address
       values:
          - acc1
          - acc2
          - acc3
          - acc4

       # Ether value range
     - domain: eth_value
       type: Int
    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:

          # step 1,2: Create accounts acc1 with 3 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 1
                value: 5

          # step 3,4: Create accounts acc2 with 3 units

        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
                beneficiary: 2
                value: 3

          # step 5: Account 'acc1' creates contract, and becomes
          # Richest (msg.value=1)

        - interface: WithdrawalContract()
          bindExact: true
          input:
              _default: 1
              value: 1
              sender: 1

        # step 6: 'acc2' becomes richest because the msg.value 3
        # exceeds previous mostSent (1 of acc1). Old richest
        # (acc1) receives msg.value.

        - interface: WithdrawalContract(becomeRichest)
          bindExact: true
          input:
              _default: 1
              value: 3
              sender: 2
              recipient: 3

             
        # step 7: 'acc1' withdraws

        - interface: WithdrawalContract(withdraw)
          bindExact: true
          input:
              _default: 1
              value: 0
              sender: 1
              recipient: 3
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
5 step p_WithdrawalContract__
6 step p_WithdrawalContract_becomeRichest_
7 step p_WithdrawalContract_withdraw_
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
2 eth_accounts acc1 balance 5
4 eth_accounts acc1 balance 5
4 eth_accounts acc2 balance 3
5 eth_accounts acc1 balance 4
5 eth_accounts acc2 balance 3
5 eth_accounts acc3 balance 1
6 eth_accounts acc1 balance 4
6 eth_accounts acc2 balance 0
6 eth_accounts acc3 balance 4
7 eth_accounts acc1 balance 7
7 eth_accounts acc2 balance 0
7 eth_accounts acc3 balance 1
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
5 eth_storageRoot acc3 richest acc1
5 eth_storageRoot acc3 mostSent 1
6 eth_storageRoot acc3 richest acc2
6 eth_storageRoot acc3 mostSent 3
7 eth_storageRoot acc3 richest acc2
7 eth_storageRoot acc3 mostSent 3
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
5 eth_storageRoot pendingWithdrawals acc1 0
5 eth_storageRoot pendingWithdrawals acc2 0
5 eth_storageRoot pendingWithdrawals acc3 0
6 eth_storageRoot pendingWithdrawals acc1 3
6 eth_storageRoot pendingWithdrawals acc2 0
6 eth_storageRoot pendingWithdrawals acc3 0
7 eth_storageRoot pendingWithdrawals acc1 0
7 eth_storageRoot pendingWithdrawals acc2 0
7 eth_storageRoot pendingWithdrawals acc3 0