How to test the given code

  • Thread starter zak100
  • Start date
  • #1
zak100
Gold Member
435
10

Main Question or Discussion Point

Hi,
I read a research paper for verification and validation of solidity code. 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? Code is given below:



Code:
  contract MyBank {

  mapping (address)==>uint) balances;

  function Deposit() {

  balances[msg.sender] += msg.value;

  }|

  function Withdraw(uint amount) {

  if(balances[msg.sender] >=amount) {

  msg.sender.send(amount);

  balances[msg.sender] -= amount;

}

}

function Balance() constant returns(uint) {

return balances[msg.sender];

}
A quick response is really appreciated.

Zulfi.
 

Answers and Replies

  • #2
11,501
5,047
I don’t know if this will help but when doing java code we can setup junit tests to exercise the code. This is a somewhat manual process best done with an IDE like Netbeans or Eclipse. Junit is a framework for writing th testcases. It doesn’t read your code and write them.

I imagine whatever you’re referring to does the same thing. You have to look at your code and write inputs that exercise the conditional and looping logic and then compare actual output to expected output.
 
  • #3
zak100
Gold Member
435
10
Hi,
Thanks for your reply.

Hi,
What I understand is that:
Initially balance is zero. Then store some value in the balance using msg.value : lets suppose 500. & lets suppose in Withdraw(700) it checks that balance is greater than amount so it sends the amount & deducts balance which seems fine. However a conversion of the code into F* is shown below (from research paper: https://www.cs.umd.edu/~aseem/solidetherplas.pdf)

Code:
module MyBank
open Solidity
type state = f balances: mapping address uint; g
val store : state = fbalances = ref empty mapg
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
and when its analyzed using F*, it gives following error:

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.

Zulfi.
 

Related Threads on How to test the given code

  • Last Post
Replies
8
Views
2K
  • Last Post
Replies
3
Views
2K
  • Last Post
Replies
1
Views
1K
Replies
1
Views
596
  • Last Post
Replies
3
Views
3K
Replies
8
Views
870
Replies
18
Views
970
Replies
3
Views
476
Replies
8
Views
4K
Top