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:
  1.	contract MyBank {
2.	mapping (address)==>uint) balances;
3.	function Deposit() {
4.	balances[msg.sender] += msg.value;
5.	}|
6.	function Withdraw(uint amount) {
7.	if(balances[msg.sender] >=amount) {
8.	msg.sender.send(amount);
9.	balances[msg.sender] -= amount;
10.	}
11.	}
12.	function Balance() constant returns(uint) {
13.	return balances[msg.sender];
14.	}
A quick response is really appreciated.

Zulfi.