I read a research paper for verification and validation of solidity code Here's a link:)!

The code is given below:

contract MyBank {
   mapping (address)uint) balances;

function Deposit() {
   balances[msg.sender] += msg.value;

function Withdraw(uint amount) {
   if(balances[msg.sender]  amount) {
     balances[msg.sender] 􀀀= amount;

function Balance() constant returns(uint) {
   return balances[msg.sender];

It uses F* (F-star). However, it has to convert the solidity code into F-star. I cant find the converter. Can some body please guide me how to manually test the code?

The conversion of code into F* is given below:

 module MyBank
 open Solidity
 type state = { balances: mapping address uint; }
 val store : state = {balances = ref empty_map}

 let deposit () : Eth unit =
    update_map store.balances msg.sender
       (add (lookup store.balances msg.sender) msg.value)

 let withdraw (amount:uint) : Eth unit =
 if (ge (lookup store.balances msg.sender) amount) then
 send msg.sender amount;
 update_map store.balances msg.sender
 (sub (lookup store.balances msg.sender) amount)

 let balance () : Eth uint =
 lookup store.balances msg.sender

What I understand is that: Initially balance is zero. Then store some value in the balance using msg.value : lets suppose 500. & in lets suppose Withdraw(700) it checks that balance is greater than amount so it sends the amount & deducts balance which seems fine. However paper says:

Using the effect system of F*, we now show how to detect some vulnerable patterns such as unchecked send results in translated contracts. The base construction is a combined exception and state monad (see [9] for details) with the following signature:

EST (a:Type) = h0:heap // input heap ->send_failed:bool // send failure flag ->Tot (option (a * heap) // result and new heap, or exception * bool) // new failure flag

return (a:Type) (x:a) : EST a = fun h0 b0->Some (x, h0), b0

bind (a:Type) (b:Type) (f:EST a) (g:a->EST b) : EST b = fun h0 b0-> match f h0 b0 with | None, b1->None, b1 // exception in f: no output heap |Some (x, h1), b1->g x h1 b1 // run g, carry failure flag

Some body please guide me how to detect the error and what the above paragraph says.


  • To start with, the Deposit is not payable so the function can't receive Ether - it will throw an error if you try to send Ether to it. – Lauri Peltonen Sep 23 '18 at 16:41
  • With all due respect to the research linked, did your try first writing tests to your contract the current "usual" way, like using Truffle and JS? truffleframework.com/docs/truffle/testing/… – Utgarda Sep 23 '18 at 17:15
  • Thanks. We have to add payable modifier to receive ether. I tried with Truffle but got some error with migrate. I would try it again. – zak100 Sep 23 '18 at 19:00

It depends what you mean by manual testing. You could paste the contract into Remix for superficial testing. http://remix.ethereum.org. That would help you discover that the deposit() function doesn't accept deposits.

It might not help you discover that the contract contains an anti-pattern and a re-entrance vulnerability because a state-change takes place after flow control is relinquished to an untrusted contract with transfer.

Truffle framework provides a mocha-based unit test framework. This supports testing to the extent that the test designer wishes to explore unintended uses to make sure the contract doesn't do anything it's not supposed to do. As you know, it does not formally assure that no defect can exist.

You may be interested in adding assert() functions to use with something like https://github.com/melonproject/oyente. The combination of assert() in the contract to indicate intent and a code analyzer may get you part way to the sort of analysis you wanted.

Hope it helps.


Smart contracts written in solidity are usually tested using mocha. Though, any other library would work.

Here's what you could do to test your smart contract using JavaScript:

  1. Compile the contract using solc.js
  2. Deploy the contract on ganache.
  3. Access the contracts functions using web3.
  4. Write unit tests using mocha and assert.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.