INVALID-TITLE
跳到导航
跳到搜索
EXAMPLE
Loan contract
Loan contract, refers to a contract where a lender delivers a certain amount of funds to a borrower, and the latter returns the same amount of funds within a certain period of time and pays interests to the lender. There are 6 terms in the contract that consists of two aspects: 1) the borrower shall submit a loan application stating the amount he/she wants to borrow, and 2) the lender may deposit funds into the contract account until the target of loan is reached. Before borrowing, the contract requires that the borrower must confirm the loan information and check the historical loan records, and then calculate the corresponding interests. Meanwhile, the contract asserts that the borrower pays off the loan amount before the loan date comes.
1 Lend Spesc.scs
2 contract Lend{
3 party User{
4 loan : Loan
5 SubmitLoanApplication(l : Loan)
6 confirm()
7 getHisLoan()
8 payback()
9 }
10
11 party Funder{
12 moneyFunded : Money
13 moneyWillGet : Money
14 Contribute(uid : User)
15 refund(uid : User)
16 }
17
18 term term1 : User can SubmitLoanApplication.
19
20 term term2 : Funder can Contribute
21 when before uid::loan::timelimit
22 while deposit $ value <= uid::loan::fundingGoal.
23
24 term term3 : Funder can refund
25 when after uid::loan::timelimit and uid::loan::amount < uid::loan::fundingGoal
26 while withdraw $ his::moneyFunded.
27
28 term term4 : User must confirm
29 when within 3 day after his::loan::timelimit and his::loan::amount = his::loan::fundingGoal.
30
31 term term5 : User can getHisLoan
32 when after User did confirm
33 while withdraw $ his::loan::amount.
34
35 term term6 : User must payback
36 when after User did confirm and before his::loan::tenorM
37 while
38 deposit $ his::loan::balance + his::loan::installment
39 transfer $ his::loan::funders::moneyWillGet to his::loan::funders.
40
41 type Loan
42 {
43 operationName : Name//use of money
44 beneficiary : User//Borrower
45 timelimit : Date//time limit of collecting money
46 fundingGoal : integer//the amount borrower want to borrow
47 amount : integer//the money collected now
48 balance : integer//the Capital have to pay back
49 numFunders : integer
50 interestRateM : integer// monthly
51 gracePeriod : integer//the period you don't have to pay the interest
52 tenorM : integer//monthly//you have to pay back tenorM month later
53 installment : integer//monthly//the interest have to pay back
54 funders : set Funder
55 }
56 }
57
58 FunderT.sol
59 pragma solidity >=0.4.0 <0.6.0;
60
61 contract FunderT{
62
63 uint moneyFunded;
64 uint moneyWillGet;
65
66 address _FunderAddress;
67 uint _max;
68
69 function funderT() public{
70 _max = now*1000;
71 }
72 function regist(address a) public {
73 _FunderAddress = a;
74 }
75
76 function getAddress() public returns (address a){
77 return _FunderAddress;
78 }
79
80 function getmoneyFunded() public returns(uint _result){
81 return moneyFunded;
82 }
83
84 function setmoneyFunded ( uint a) public{
85 moneyFunded = a;
86 }
87
88 /* function getmoneyWillGet() public returns(uint _result){
89 return moneyWillGet;
90 }
91
92 function setmoneyWillGet(uint a) public {
93 moneyWillGet = a;
94 }*/
95
96
97
98 function setmoneyWillGet(uint256 newValue) public {
99 moneyWillGet = newValue;
100 }
101
102
103 function getmoneyWillGet() public view returns (uint256) {
104 return moneyWillGet;
105 }
106 }
107
108 Lend.sol
109 pragma solidity >=0.4.0 <0.6.0;
110 pragma experimental ABIEncoderV2;
111
112 import "./UserT.sol";
113 import "./FunderT.sol";
114
115 contract Lend {
116
117 UserT User;
118 FunderT Funder;
119 uint start;
120
121
122 mapping (string => Loan) loan;
123
124 struct Loan{
125 bytes32 operationName;
126 address beneficiary;
127 uint timelimit;
128 uint fundingGoal;
129 uint amount;
130 uint balance;
131 uint numFunders;
132 uint interestRateM;
133 uint gracePeriod;
134 uint tenorM;
135 uint installment;
136 address funders;
137 }
138
139
140
141 constructor() public{
142 start = now;
143 User = new UserT();
144 Funder = new FunderT();
145 }
146
147 /* constructor() public{
148 start = now;
149 User = new UserT();
150 Funder = new FunderT();
151 }*/
152
153 modifier onlyUser{
154 require(User.getAddress()==msg.sender);
155 _;
156 }
157
158 modifier onlyFunder{
159 require(Funder.getAddress()==msg.sender);
160 _;
161 }
162
163 modifier term2Modifier(UserT uid){
164 // require(now < uid.loan.timelimit);
165 // require(msg.value <= uid.loan.fundingGoal);
166 _;
167 }
168
169 modifier term3Modifier(UserT uid){
170 // require(now > (uid.loan.timelimit && uid.loan.amount < uid.loan.fundingGoal));
171 _;
172 }
173
174 modifier term4Modifier{
175 // require((now > (User.getloan.timelimit(msg.sender) && User.getloan.amount(msg.sender) == User.getloan.fundingGoal(msg.sender))) &&(now < (User.getloan.timelimit(msg.sender) && User.getloan.amount(msg.sender) == User.getloan.fundingGoal(msg.sender))+259200));
176 _;
177 }
178
179 modifier term5Modifier{
180 require(now > User.confirmTime());
181 _;
182 }
183
184 modifier term6Modifier{
185 // require(now > (User.confirmTime() && now < User.getloan.tenorM(msg.sender)));
186 // require(User.getloan.balance(msg.sender) + User.getloan.installment(msg.sender));
187 _;
188 }
189
190 function SubmitLoanApplication( Loan memory l) onlyUser() public {
191 //USER CODE HERE
192 //CHECK
193
194 }
195
196 function Contribute(UserT uid) onlyFunder() term2Modifier(uid) public payable {
197 //USER CODE HERE
198 //CHECK
199
200 }
201
202 function refund(UserT uid) onlyFunder() term3Modifier(uid) public payable {
203 //USER CODE HERE
204 msg.sender.transfer(Funder.getmoneyFunded());
205 //CHECK
206
207 }
208
209 function confirm() onlyUser() term4Modifier() public {
210 //USER CODE HERE
211 //CHECK
212
213 }
214
215 function getHisLoan() onlyUser() term5Modifier() public payable {
216 //USER CODE HERE
217 msg.sender.transfer(User.getloan().amount);
218 //CHECK
219
220 }
221
222 function payback() onlyUser() term6Modifier() public payable {
223 //USER CODE HERE
224 //User.getloan().funders.transfer(msg.sender);
225 msg.sender.transfer(User.getloan().amount);
226 //CHECK
227
228 }
229
230 }
231
232 UserT.sol
233 pragma solidity >=0.4.0 <0.6.0;
234 pragma experimental ABIEncoderV2;
235
236
237 import "./Lend.sol";
238
239 contract UserT{
240
241 struct Loan{
242 bytes32 operationName;
243 address beneficiary;
244 uint timelimit;
245 uint fundingGoal;
246 uint amount;
247 uint balance;
248 uint numFunders;
249 uint interestRateM;
250 uint gracePeriod;
251 uint tenorM;
252 uint installment;
253 address funders;
254 }
255
256
257
258
259 Loan loan;
260 //attributes of actionconfirm
261 bool _isconfirmDone;
262 uint _confirmTime;
263
264 address _UserAddress;
265 uint _max;
266
267 constructor ()public{
268 _max = now*1000;
269 }
270
271 function regist(address a) public {
272 _UserAddress = a;
273 }
274
275 function getAddress() public returns (address a){
276 return _UserAddress;
277 }
278
279 function getloan() public returns(Loan memory _result) {
280 return loan;
281 }
282
283 function setloan(Loan memory a) public{
284 loan = a;
285 }
286
287 function confirmDone() public{
288 _confirmTime = now;
289 _isconfirmDone = true;
290 }
291
292 function confirmTime() public returns (uint result){
293 if(_isconfirmDone){
294 return _confirmTime;
295 }
296 return _max;
297 }
298
299 }
Auction contract
Auction contract involves two parties: auctioneer who is an enterprise legal person engaged in auction activities, and bidders who are some citizens, legal persons or organizations to participate in bidding for auction targets. The highest bidding process is described as the following steps. The auctioneer starts the auction system after setting a reserve price and an auction end time, and waits for the auction to end; The bidders can bid anytime during the system. If the bid is greater than the current highest price, the system records it as new highest price, puts the bid into the fund pool, and returns the bid paid by the previous highest bidder; otherwise, the bidder fails and the bid is returned; After the auction time is over, the auctioneer can collect the highest bid from the fund pool.
1 Simple Auction.scs
2 contract SimpleAuction{
3 party group bidders{
4 amount : Money
5 Bid()
6 withdrawOverbidMoney()
7 }
8
9 party auctioneer{
10 StartBidding(reservePrice : Money, biddingTime : Date)
11 StopBidding()
12 }
13
14 highestPrice : Money
15 highestBidder : biddersBiddingStop
16 Time : Date
17
18 term no1 : auctioneer can StartBidding,
19 when before auctioneer did StartBidding
20 where highestPrice = reservePrice and BiddingStopTime = biddingTime + now.
21
22 term no2 : bidders can Bid,
23 when after auctioneer did StartBidding and before BiddingStopTime
24 while deposit $ value > highestPrice
25 where highestPrice = value and highestBidder = this bidder and
26 this bidder : : amount = this bidder: :0ri amount + value .
27
28 term no3_1 : bidders can withdrawOverbidMoney,
29 when this bidder isn't highestBidder and this bidder: :amount > 0
30 while withdraw $this bidder : :amount
31 where this bidder : : amount = 0.
32
33
34 term no3_2 : bidders can withdrawOverbidMoney,
35 when this bidder is highestBidder and this bidder : : amount > highestPrice
36 while withdraw $this bidder : : amount - highestPrice
37 where this bidder : : amount = highestPrice.
38
39 term no4 : auctioneer can StopBidding,
40 when after BiddingStopTime and before auctioneer did StopBidding
41 while withdraw $highestPrice.
42 }
43
44 auctioneerT.sol
45 pragma solidity >=0.4.0 <0.6.0;
46
47 contract auctioneerT{
48
49
50 //attributes of actionStartBidding
51 bool _isStartBiddingDone;
52 uint _StartBiddingTime;
53
54 //attributes of actionCollectPayment
55 bool _isCollectPaymentDone;
56 uint _CollectPaymentTime;
57
58 address _auctioneerAddress;
59 uint _max;
60
61 constructor() public{
62 _max = now*1000;
63 }
64
65 function regist(address a) public {
66 _auctioneerAddress = a;
67 }
68
69 function getAddress() public returns (address a){
70 return _auctioneerAddress;
71 }
72
73 function StartBiddingDone() public{
74 _StartBiddingTime = now;
75 _isStartBiddingDone = true;
76 }
77
78 function StartBiddingTime() public returns (uint result){
79 if(_isStartBiddingDone){
80 return _StartBiddingTime;
81 }
82 return _max;
83 }
84
85 function CollectPaymentDone() public{
86 _CollectPaymentTime = now;
87 _isCollectPaymentDone = true;
88 }
89
90 function CollectPaymentTime() public returns (uint result){
91 if(_isCollectPaymentDone){
92 return _CollectPaymentTime;
93 }
94 return _max;
95 }
96
97 }
98
99 biddersT.sol
100 pragma solidity ^0.4.22;
101
102 contract biddersT{
103
104 struct bidderstype{
105 uint amount;
106
107 //attributes of actionBid
108 bool _isBidDone;
109 uint _BidTime;
110
111 //attributes of actionWithdrawOverbidMoney
112 bool _isWithdrawOverbidMoneyDone;
113 uint _WithdrawOverbidMoneyTime;
114
115 }
116
117 uint _max;//time max
118 uint _sum;//total member of this party
119 uint _BidDoneNum;
120 uint[] _BidTime;
121
122 uint _WithdrawOverbidMoneyDoneNum;
123 uint[] _WithdrawOverbidMoneyTime;
124
125 bidderstype _Empty;//used to initialize
126 bidderstype[] _biddersEntity;
127 address[] _biddersAddress;
128 mapping(address=>uint) _userlist;
129
130 function biddersT(){
131 _BidDoneNum = 0;
132
133 _WithdrawOverbidMoneyDoneNum = 0;
134
135 _biddersEntity.push(_Empty);
136 _max = now*1000;
137 }
138
139 function getSum() public returns(uint c){
140 return _sum;
141 }
142
143 function add(address a) public {
144 _biddersEntity.push(_Empty);
145 _biddersAddress.push(a);
146 // _userlist[address] = _sum;
147
148 _sum ++;
149 }
150
151 function remove(address a) public {
152 uint num = _userlist[a];
153 _biddersEntity[num] = _biddersEntity[_sum-1];
154 delete(_biddersEntity[num]);
155 delete(_userlist[a]);
156 _sum --;
157 }
158
159 function getList() public returns (address[] a){
160 return _biddersAddress;
161 }
162
163 function contains(address a) public returns (bool b){
164 return _userlist[a] != 0;
165 }
166
167 function getamount(address a) returns(uint _result){
168 uint num = _userlist[a];
169 return _biddersEntity[num].amount;
170 }
171
172 function setamount(address a, uint b){
173 uint num = _userlist[a];
174 _biddersEntity[num].amount = b;
175 }
176
177 function BidDone(address a){
178 uint num = _userlist[a];
179 _biddersEntity[num]._BidTime = now;
180 _biddersEntity[num]._isBidDone = true;
181 _BidTime.push(_biddersEntity[num]._BidTime);
182 _BidDoneNum ++;
183 }
184
185 function BidTime(address a) returns (uint result){
186 uint num = _userlist[a];
187 if(_biddersEntity[num]._isBidDone){
188 return _biddersEntity[num]._BidTime;
189 }
190 return _max;
191 }
192
193 function BidAllTime() returns (uint result){
194 if(_BidDoneNum == _max-1){
195 return _BidTime[_BidDoneNum-1];
196 }
197 return _max;
198 }
199
200 function BidSomeTime() returns (uint result){
201 if(_BidDoneNum >= 1){
202 return _BidTime[0];
203 }
204 return _max;
205 }
206
207 function WithdrawOverbidMoneyDone(address a){
208 uint num = _userlist[a];
209 _biddersEntity[num]._WithdrawOverbidMoneyTime = now;
210 _biddersEntity[num]._isWithdrawOverbidMoneyDone = true;
211 _WithdrawOverbidMoneyTime.push(_biddersEntity[num]._WithdrawOverbidMoneyTime);
212 _WithdrawOverbidMoneyDoneNum ++;
213 }
214
215 function WithdrawOverbidMoneyTime(address a) returns (uint result){
216 uint num = _userlist[a];
217 if(_biddersEntity[num]._isWithdrawOverbidMoneyDone){
218 return _biddersEntity[num]._WithdrawOverbidMoneyTime;
219 }
220 return _max;
221 }
222
223 function WithdrawOverbidMoneyAllTime() returns (uint result){
224 if(_WithdrawOverbidMoneyDoneNum == _max-1){
225 return _WithdrawOverbidMoneyTime[_WithdrawOverbidMoneyDoneNum-1];
226 }
227 return _max;
228 }
229
230 function WithdrawOverbidMoneySomeTime() returns (uint result){
231 if(_WithdrawOverbidMoneyDoneNum >= 1){
232 return _WithdrawOverbidMoneyTime[0];
233 }
234 return _max;
235 }
236
237 }
238
239 goodsOwnerT.sol
240 pragma solidity ^0.4.22;
241
242 contract goodsOwnerT{
243
244
245 //attributes of actionStartBidding
246 bool _isStartBiddingDone;
247 uint _StartBiddingTime;
248 bool _isgoodsOwnerDone;
249
250 uint _max;
251
252 //attributes of actionStopBidding
253 bool _isStopBiddingDone;
254 uint _StopBiddingTime;
255
256 address[] _goodsOwnerAddress;
257
258 constructor() public{
259 _max = now*1000;
260 }
261
262 function regist (address[] a){
263 _goodsOwnerAddress = a;
264 }
265
266 function getAddress() public returns (address[] a){
267 return _goodsOwnerAddress;
268 }
269
270 function StartBiddingDone(address[] a){
271 // StartBiddingTime = now;
272 _isgoodsOwnerDone = true;
273 //_isStartBiddingDone = true;
274 }
275
276 function StartBiddingTime() returns (uint result){
277 if(_isStartBiddingDone){
278 return _StartBiddingTime;
279 }
280 return _max;
281 }
282
283 function StopBiddingDone(address[] a){
284 // StopBiddingTime = now;
285 _isgoodsOwnerDone = true;
286 // _StopBiddingTime = true;
287 }
288
289 function StopBiddingTime() returns (uint result){
290 if(_isStopBiddingDone){
291 return _StopBiddingTime;
292 }
293 return _max;
294 }
295
296 }
297
298 SimpleAuction.sol
299 pragma solidity ^0.4.22;
300
301 contract SimpleAuction {
302
303 address public beneficiary;
304 uint public auctionEnd;
305 address public highestBidder;
306 uint public highestBid;
307 mapping(address => uint) pendingReturns;
308 bool ended;
309
310 event HighestBidIncreased(address bidder, uint amount);
311 event AuctionEnded(address winner, uint amount);
312
313 constructor(uint _biddingTime, address _beneficiary) public {
314 beneficiary = _beneficiary;
315 auctionEnd = now + _biddingTime;
316 }
317
318 function bid() public payable {
319
320 require(now <= auctionEnd, "Auction already ended.");
321 require(msg.value > highestBid, "There already is a higher bid.");
322
323 if (highestBid != 0) {
324 pendingReturns[highestBidder] += highestBid;
325 }
326 highestBidder = msg.sender;
327 highestBid = msg.value;
328 HighestBidIncreased(msg.sender, msg.value);
329 }
330
331 function withdraw() public returns (bool) {
332 uint amount = pendingReturns[msg.sender];
333 if (amount > 0) {
334 pendingReturns[msg.sender] = 0;
335
336 if (!msg.sender.send(amount)) {
337 // No need to call throw here, just reset the amount owing
338 pendingReturns[msg.sender] = amount;
339 return false;
340 }
341 }
342 return true;
343 }
344
345 function auctionEnd() public {
346
347 require(now >= auctionEnd, "Auction not yet ended.");
348 require(!ended, "auctionEnd has already been called.");
349
350 ended = true;
351 AuctionEnded(highestBidder, highestBid);
352
353 beneficiary.transfer(highestBid);
354 }
355 }
House-leasing contract
House-leasing contract, takes assets as the transaction subject between lessor and lessee. There are 7 terms in the contract, including two aspects: 1) the lessor can register the house after depositing the rental deposit, and 2) the lessee can keep the right to use the house during the leasing period after depositing the rent. After confirming the leased house, the contract requires that the lessee shall pay the rent, and the lessor must transfer the right to the lessee within one week. Meanwhile, the contract stipulates the pre-condition for the lessor to charge the rent paid by the lessee, and the postcondition for both parties to get their deposits back after the house inspection.
1 HouseLease.scs
2 contract Houselease{
3 party Renter{
4 registerHouse()
5 collectRent()
6 collectBail()
7 transferHouse()
8 checkHouse()
9 }
10
11 party Tenant{
12 confirmLease(endLeasingDuration:Date,
13 payDuration:Date)
14 payRent()
15 returnHouse()
16 collectBail()
17 }
18
19 house : House
20 infos : contractInfo
21
22 term term1 : Renter can registerHouse
23 while deposit $infos::renterBail.
24
25 term term2 : Tenant can confirmLease
26 when after Renter did registerHouse
27 while deposit $infos::tenantBail
28 where infos::startLeasingTime = now and
29 infos::endLeasingTime = endLeasingDuration + now
30 and infos::payDate = payDuration + now
31 and infos::payDuration = payDuration.
32
33 term term3 : Renter must transferHouse
34 when within 7 day after Tenant did confirmLease
35 while deposit $ house::useRight.
36
37 term term4 : Tenant must payRent
38 when before Tenant did confirmLease
39 while deposit $infos::rental
40 withdraw $house::useRight
41 where infos::payDate = infos::payDate + infos::payDuration
42 and infos::totalRental = infos::totalRental + infos::rental.
43
44 term term5 : Renter can collectRent
45 while withdraw $infos::totalRental
46 where infos::totalRental = 0.
47
48 term term6 : Tenant must returnHouse
49 when within 7 day after Renter did checkHouse
50 while deposit $house::useRight
51 transfer $house::useRight to Renter.
52
53 term term7_1 : Renter can collectBail
54 when within 15 day after Renter did checkHouse
55 while withdraw $infos::renterBail.
56
57 term term7_2 : Tenant can collectBail
58 when within 15 day after Renter did checkHouse
59 while withdraw $infos::tenantBail.
60
61 type contractInfo {
62 renterBail : Money
63 tenantBail : Money
64 rental : Money
65 totalRental : Money
66 penalty : Money
67 startLeasingTime : Date
68 endLeasingTime : Date
69 payDate : Date
70 payDuration : Date
71 }
72
73 type House {
74 ownershipNumber : integer
75 location : String
76 area : integer
77 usage : String
78 price : Money
79 useRight : String
80 usufruct : String
81 dispositionRight : String
82 possessionRight : String
83 }
84 }
85
86 Houselease.sol
87 pragma solidity ^0.4.0;
88
89 import "./RenterT.sol";
90 import "./TenantT.sol";
91
92 contract Houselease {
93
94 RenterT Renter;
95 TenantT Tenant;
96
97 House house;
98 contractInfo infos;
99
100 uint start;
101 struct contractInfo{
102 uint renterBail;
103 uint tenantBail;
104 uint rental;
105 uint totalRental;
106 uint penalty;
107 uint startLeasingTime;
108 uint endLeasingTime;
109 uint payDate;
110 uint payDuration;
111 }
112 struct House{
113 uint ownershipNumber;
114 bytes32 location;
115 uint area;
116 bytes32 usage;
117 uint price;
118 uint useRight;
119 uint usufruct;
120 uint dispositionRight;
121 uint possessionRight;
122 }
123
124 function Houselease(){
125 start = now;
126 Renter = new RenterT();
127 Tenant = new TenantT();
128 }
129
130 modifier onlyRenter{
131 require(Renter.contains(msg.sender));
132 _;
133 }
134
135 modifier onlyTenant{
136 require(Tenant.contains(msg.sender));
137 _;
138 }
139
140 modifier term2Modifier{
141 require(now > Renter.registerHouseTime());
142 require(infos.tenantBail > 0);
143 _;
144 }
145
146 modifier term3Modifier{
147 require((now > Tenant.confirmLeaseTime()) &&(now < Tenant.confirmLeaseTime()+604800));
148 require(house.useRight > 0);
149 _;
150 }
151
152 modifier term4Modifier{
153 require(now < Tenant.confirmLeaseTime());
154 require(infos.rental > 0);
155 _;
156 }
157
158 modifier term6Modifier{
159 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+604800));
160 require(house.useRight > 0);
161 _;
162 }
163
164 modifier term7_1Modifier{
165 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+1296000));
166 _;
167 }
168
169 modifier term7_2Modifier{
170 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+1296000));
171 _;
172 }
173
174 function registerHouse() onlyRenter() public payable {
175 //USER CODE HERE
176 //CHECK
177
178 }
179
180 function confirmLease(uint endLeasingDuration, uint payDuration) onlyTenant() term2Modifier() public payable {
181 //USER CODE HERE
182 infos.startLeasingTime = now;
183 infos.endLeasingTime = endLeasingDuration + now;
184 infos.payDate = payDuration + now;
185 infos.payDuration = payDuration;
186 //CHECK
187 assert(infos.startLeasingTime == now && (infos.endLeasingTime == endLeasingDuration + now && (infos.payDate == payDuration + now && infos.payDuration == payDuration)));
188 }
189
190 function transferHouse() onlyRenter() term3Modifier() public payable {
191 //USER CODE HERE
192 //CHECK
193
194 }
195
196 function payRent() onlyTenant() term4Modifier() public payable {
197 //USER CODE HERE
198 infos.payDate = infos.payDate + infos.payDuration;
199 infos.totalRental = infos.totalRental + infos.rental;
200 msg.sender.transfer(house.useRight);
201 //CHECK
202 assert(infos.payDate == infos.payDate + infos.payDuration && infos.totalRental == infos.totalRental + infos.rental);
203 }
204
205 function collectRent() onlyRenter() term7_1Modifier() public payable {
206 //USER CODE HERE
207 infos.totalRental = 0;
208 msg.sender.transfer(infos.totalRental);
209 //CHECK
210 assert(infos.totalRental == 0);
211 }
212
213 function returnHouse() onlyTenant() term6Modifier() public payable {
214 //USER CODE HERE
215 address(Renter).transfer(house.useRight);
216 //CHECK
217
218 }
219
220 }
221
222 RenterT.sol
223 pragma solidity ^0.4.22;
224
225 contract RenterT{
226
227
228 //attributes of actionregisterHouse
229 bool _isregisterHouseDone;
230 uint _registerHouseTime;
231
232 //attributes of actioncollectRent
233 bool _iscollectRentDone;
234 uint _collectRentTime;
235
236 //attributes of actioncollectBail
237 bool _iscollectBailDone;
238 uint _collectBailTime;
239
240 //attributes of actiontransferHouse
241 bool _istransferHouseDone;
242 uint _transferHouseTime;
243
244 //attributes of actioncheckHouse
245 bool _ischeckHouseDone;
246 uint _checkHouseTime;
247
248 uint _max;
249 bool _isRenterDone;
250 uint _i;
251
252 address[] _RenterAddress;
253 function RenterT(){
254 _max = now*1000;
255 }
256
257 function regist(address a) public {
258 _RenterAddress[_i] = a;
259 _i++;
260 }
261
262 function getAddress(uint _i) public returns (address a){
263 return _RenterAddress[_i];
264 }
265
266 function registerHouseDone(address a){
267 _registerHouseTime = now;
268 _isRenterDone = true;
269 }
270
271 function registerHouseTime() returns (uint result){
272 if(_isregisterHouseDone){
273 return _registerHouseTime;
274 }
275 return _max;
276 }
277
278 function collectRentDone(address a){
279 _collectRentTime = now;
280 _isRenterDone = true;
281 }
282
283 function collectRentTime() returns (uint result){
284 if(_iscollectRentDone){
285 return _collectRentTime;
286 }
287 return _max;
288 }
289
290 function collectBailDone(address a){
291 _collectBailTime = now;
292 _isRenterDone = true;
293 }
294
295 function collectBailTime() returns (uint result){
296 if(_iscollectBailDone){
297 return _collectBailTime;
298 }
299 return _max;
300 }
301
302 function transferHouseDone(address a){
303 _transferHouseTime = now;
304 _isRenterDone = true;
305 }
306
307 function transferHouseTime() returns (uint result){
308 if(_istransferHouseDone){
309 return _transferHouseTime;
310 }
311 return _max;
312 }
313
314 function checkHouseDone(address a){
315 _checkHouseTime = now;
316 _isRenterDone = true;
317 }
318
319 function checkHouseTime() returns (uint result){
320 if(_ischeckHouseDone){
321 return _checkHouseTime;
322 }
323 return _max;
324 }
325
326 function contains(address a) returns (bool result) {
327 for (uint _j = 0; _j < _RenterAddress.length; _j++ ) { //for loop example
328 if (a == _RenterAddress[_j]){
329 return true;
330 }
331 }
332 return false;
333 }
334
335 }
336
337 TenantT.sol
338 pragma solidity ^0.4.22;
339
340 contract TenantT{
341
342
343 //attributes of actionconfirmLease
344 bool _isconfirmLeaseDone;
345 uint _confirmLeaseTime;
346
347 //attributes of actionpayRent
348 bool _ispayRentDone;
349 uint _payRentTime;
350
351 //attributes of actionreturnHouse
352 bool _isreturnHouseDone;
353 uint _returnHouseTime;
354
355 //attributes of actioncollectBail
356 bool _iscollectBailDone;
357 uint _collectBailTime;
358
359 uint _max;
360 bool _isTenantDone;
361 uint _i;
362
363 address[] _TenantAddress;
364 function TenantT(){
365 _max = now*1000;
366 }
367
368 function regist(address a) public {
369 _TenantAddress[_i] = a;
370 _i++;
371 }
372
373 function getAddress(uint _i) public returns (address a){
374 return _TenantAddress[_i];
375 }
376
377 function confirmLeaseDone(address a){
378 _confirmLeaseTime = now;
379 _isTenantDone = true;
380 }
381
382 function confirmLeaseTime() returns (uint result){
383 if(_isconfirmLeaseDone){
384 return _confirmLeaseTime;
385 }
386 return _max;
387 }
388
389 function payRentDone(address a){
390 _payRentTime = now;
391 _isTenantDone = true;
392 }
393
394 function payRentTime() returns (uint result){
395 if(_ispayRentDone){
396 return _payRentTime;
397 }
398 return _max;
399 }
400
401 function returnHouseDone(address a){
402 _returnHouseTime = now;
403 _isTenantDone = true;
404 }
405
406 function returnHouseTime() returns (uint result){
407 if(_isreturnHouseDone){
408 return _returnHouseTime;
409 }
410 return _max;
411 }
412
413 function collectBailDone(address a){
414 _collectBailTime = now;
415 _isTenantDone = true;
416 }
417
418 function collectBailTime() returns (uint result){
419 if(_iscollectBailDone){
420 return _collectBailTime;
421 }
422 return _max;
423 }
424
425 function contains(address a) returns (bool result) {
426 for (uint _j = 0; _j < _TenantAddress.length; _j++ ) { //for loop example
427 if (a == _TenantAddress[_j]){
428 return true;
429 }
430 }
431 return false;
432 }
433
434 }
Purchase contract
Purchase contract, transfers the ownership of goods from a seller to a buyer through logistics company. There are 10 terms in the contract, including three parts: 1) once the goods are confirmed, the seller will sign a contract and take twice the contracting price as the delivery price, 2) the goods are sent to the buyer through logistics when the buyer purchases the goods, and 3) only when the logistics successfully delivers the goods to the buyer can the seller get back the payment. According to relevant laws, the contract requires the buyer can apply for compensation if goods do not arrive within 10 days after payment, or the seller can automatically confirm the arrival if the buyer does not confirm or apply for refund within 7 days after arrival.
1 purchase.scs
2 contract Purchase{
3 party seller{
4 //定义seller角色,有四个动作
5 create()
6 abort()
7 confirmClaim()
8 autoConfirm()
9 }
10
11 party buyer{
12 confirmPurchase()//
13 confirmReceived()
14 overtimeClaim()
15 claim()
16 revokeClaim()
17 }
18
19 party logistics{
20 //第三方角色,物流公司
21 arrive()
22 }
23
24 balance : integer
25
26 xxxDescription : goods//定义一个商品描述,good是下面定义的商品结构体
27
28 term no1 : seller can create
29 while deposit $ xxxDescription::price*2.
30 //卖家可以创建合约,同时要存入物品两倍价格作为保证金
31
32 term no2 : buyer can confirmPurchase
33 when after seller did create
34 while deposit $ xxxDescription::price*2.
35 //买家创建合约后买家可以确认购买,同时要存入物品两倍价格作为保证金和货款
36
37 term no3 : seller can abort
38 when before buyer did confirmPurchase
39 while withdraw $ xxxDescription::price*2.
40 //卖家在买家确认购买之前,可以撤回合约,并取走两倍的保证金
41
42 term no4 : logistics must arrive
43 when within 10 day after buyer did confirmPurchase.
44 //买家付款后10天内必须到货
45
46 term no5 : buyer must confirmReceived
47 when within 7 day after logistics did arrive
48 while
49 withdraw $ xxxDescription::price
50 transfer $ balance to seller.
51 //买家在到货后7天内必须确认到货,同时双方取走保证金,卖家取走货款
52
53 term no6 : buyer can claim
54 when within 7 day after logistics did arrive.
55 //买家可以在到货7天内申请赔款
56
57 term no7 : buyer can overtimeClaim
58 when after start + 10 day or after logistics did arrive.
59 //如果货物在付款后10天内没到,买家可以申请赔款
60
61 term no8 : seller can confirmClaim
62 when after buyer did claim or after buyer did overtimeClaim
63 while transfer $ balance to buyer.
64 //卖家可以同意退款,并把所有保证金及货款转给买家
65
66 term no9 : buyer can revokeClaim
67 when after buyer did claim or after buyer did overtimeClaim
68 while
69 withdraw $ xxxDescription::price
70 transfer $ balance to seller.
71 //买家可以撤回退款申请
72
73 term no10 : seller can autoConfirm
74 when before buyer did claim and 7 day after logistics did arrive
75 while
76 withdraw $ xxxDescription::price
77 transfer $ balance to seller.
78 //如果到货七天内买家没有确认或申请退款,卖家可以自动确认到货。
79
80 type goods {
81 name : Name//物品名称
82 quantity : integer//物品数量
83 price : Money//价格
84 package : String//运送包装
85 }
86 }
87
88 buyerT.sol
89 pragma solidity ^0.4.22;
90
91 contract buyerT{
92
93
94 //attributes of actionconfirmPurchase
95 bool _isconfirmPurchaseDone;
96 uint _confirmPurchaseTime;
97
98 //attributes of actionconfirmReceived
99 bool _isconfirmReceivedDone;
100 uint _confirmReceivedTime;
101
102 //attributes of actionovertimeClaim
103 bool _isovertimeClaimDone;
104 uint _overtimeClaimTime;
105
106 //attributes of actionclaim
107 bool _isclaimDone;
108 uint _claimTime;
109
110 //attributes of actionrevokeClaim
111 bool _isrevokeClaimDone;
112 uint _revokeClaimTime;
113
114 uint _max;
115 bool _isbuyerDone;
116 uint _i = 0;
117
118 address[] _buyerAddress;
119 function buyerT(){
120 _max = now*1000;
121 }
122
123 function regist(address a) public {
124 _buyerAddress[_i] = a;
125 _i++;
126 }
127
128 function getAddress() public returns (address a){
129 return _buyerAddress[_i];
130 }
131
132 function confirmPurchaseDone(address a){
133 _confirmPurchaseTime = now;
134 _isbuyerDone = true;
135 }
136
137 function confirmPurchaseTime() returns (uint result){
138 if(_isconfirmPurchaseDone){
139 return _confirmPurchaseTime;
140 }
141 return _max;
142 }
143
144 function confirmReceivedDone(address a){
145 _confirmReceivedTime = now;
146 _isbuyerDone = true;
147 }
148
149 function confirmReceivedTime() returns (uint result){
150 if(_isconfirmReceivedDone){
151 return _confirmReceivedTime;
152 }
153 return _max;
154 }
155
156 function overtimeClaimDone(address a){
157 _overtimeClaimTime = now;
158 _isbuyerDone = true;
159 }
160
161 function overtimeClaimTime() returns (uint result){
162 if(_isovertimeClaimDone){
163 return _overtimeClaimTime;
164 }
165 return _max;
166 }
167
168 function claimDone(address a){
169 _claimTime = now;
170 _isbuyerDone = true;
171 }
172
173 function claimTime() returns (uint result){
174 if(_isclaimDone){
175 return _claimTime;
176 }
177 return _max;
178 }
179
180 function revokeClaimDone(address a){
181 _revokeClaimTime = now;
182 _isbuyerDone = true;
183 }
184
185 function revokeClaimTime() returns (uint result){
186 if(_isrevokeClaimDone){
187 return _revokeClaimTime;
188 }
189 return _max;
190 }
191
192 function contains(address a) returns (bool result) {
193 for (uint _j = 0; _j < _buyerAddress.length; _j++ ) { //for loop example
194 if (a == _buyerAddress[_j]){
195 return true;
196 }
197 }
198 return false;
199 }
200
201 }
202
203 logisticsT.sol
204 pragma solidity ^0.4.22;
205
206 contract logisticsT{
207
208
209 //attributes of actionarrive
210 bool _isarriveDone;
211 uint _arriveTime;
212
213 uint _max;
214 bool _islogisticsDone;
215 uint _i = 0;
216
217 address[] _logisticsAddress;
218 function logisticsT(){
219 _max = now*1000;
220 }
221
222 function regist(address a) public {
223 _logisticsAddress[_i] = a;
224 }
225
226 function getAddress() public returns (address a){
227 return _logisticsAddress[_i];
228 }
229
230 function arriveDone(address a){
231 _arriveTime = now;
232 _islogisticsDone = true;
233 }
234
235 function arriveTime() returns (uint result){
236 if(_isarriveDone){
237 return _arriveTime;
238 }
239 return _max;
240 }
241
242 function contains(address a) returns (bool result) {
243 for (uint _j = 0; _j < _logisticsAddress.length; _j++ ) { //for loop example
244 if (a == _logisticsAddress[_j]){
245 return true;
246 }
247 }
248 return false;
249 }
250
251 }
252
253 Purchase.sol
254 pragma solidity ^0.4.0;
255
256 import "./sellerT.sol";
257 import "./buyerT.sol";
258 import "./logisticsT.sol";
259
260 contract Purchase {
261
262 sellerT seller;
263 buyerT buyer;
264 logisticsT logistics;
265
266 uint balance;
267 goods xxxDescription;
268
269 uint start;
270 struct goods{
271 bytes32 name;
272 uint quantity;
273 uint price;
274 bytes32 package;
275 }
276
277 function Purchase(){
278 start = now;
279 seller = new sellerT();
280 buyer = new buyerT();
281 logistics = new logisticsT();
282 }
283
284 modifier onlyseller{
285 require(seller.contains(msg.sender));
286 _;
287 }
288
289 modifier onlybuyer{
290 require(buyer.contains(msg.sender));
291 _;
292 }
293
294 modifier onlylogistics{
295 require(logistics.contains(msg.sender));
296 _;
297 }
298
299 modifier no2Modifier{
300 require(now > seller.createTime());
301 require(xxxDescription.price * 2 > 0);
302 _;
303 }
304
305 modifier no3Modifier{
306 require(now < buyer.confirmPurchaseTime());
307 _;
308 }
309
310 modifier no4Modifier{
311 require((now > buyer.confirmPurchaseTime()) &&(now < buyer.confirmPurchaseTime()+864000));
312 _;
313 }
314
315 modifier no5Modifier{
316 require((now > logistics.arriveTime()) &&(now < logistics.arriveTime()+604800));
317 _;
318 }
319
320 modifier no6Modifier{
321 require((now > logistics.arriveTime()) &&(now < logistics.arriveTime()+604800));
322 _;
323 }
324
325 modifier no7Modifier{
326 require(now > start + 864000 || now > logistics.arriveTime());
327 _;
328 }
329
330 modifier no8Modifier{
331 require(now > buyer.claimTime() || now > buyer.overtimeClaimTime());
332 _;
333 }
334
335 modifier no9Modifier{
336 require(now > buyer.claimTime() || now > buyer.overtimeClaimTime());
337 _;
338 }
339
340 modifier no10Modifier{
341 require(now < buyer.claimTime() && now > logistics.arriveTime()+604800);
342 _;
343 }
344
345 function create() onlyseller() public payable {
346 //USER CODE HERE
347 //CHECK
348
349 }
350
351 function confirmPurchase() onlybuyer() no2Modifier() public payable {
352 //USER CODE HERE
353 //CHECK
354
355 }
356
357 function abort() onlyseller() no3Modifier() public payable {
358 //USER CODE HERE
359 msg.sender.transfer(xxxDescription.price * 2);
360 //CHECK
361
362 }
363
364 function arrive() onlylogistics() no4Modifier() public {
365 //USER CODE HERE
366 //CHECK
367
368 }
369
370 function confirmReceived() onlybuyer() no5Modifier() public payable {
371 //USER CODE HERE
372 msg.sender.transfer(xxxDescription.price);
373 address(seller).transfer(balance);
374 //CHECK
375
376 }
377
378 function claim() onlybuyer() no6Modifier() public {
379 //USER CODE HERE
380 //CHECK
381
382 }
383
384 function overtimeClaim() onlybuyer() no7Modifier() public {
385 //USER CODE HERE
386 //CHECK
387
388 }
389
390 function confirmClaim() onlyseller() no8Modifier() public payable {
391 //USER CODE HERE
392 address(buyer).transfer(balance);
393 //CHECK
394
395 }
396
397 function revokeClaim() onlybuyer() no9Modifier() public payable {
398 //USER CODE HERE
399 msg.sender.transfer(xxxDescription.price);
400 address(seller).transfer(balance);
401 //CHECK
402
403 }
404
405 function autoConfirm() onlyseller() no10Modifier() public payable {
406 //USER CODE HERE
407 msg.sender.transfer(xxxDescription.price);
408 address(seller).transfer(balance);
409 //CHECK
410
411 }
412
413 }
414
415 sellerT.sol
416 pragma solidity ^0.4.22;
417
418 contract sellerT{
419
420
421 //attributes of actioncreate
422 bool _iscreateDone;
423 uint _createTime;
424
425 //attributes of actionabort
426 bool _isabortDone;
427 uint _abortTime;
428
429 //attributes of actionconfirmClaim
430 bool _isconfirmClaimDone;
431 uint _confirmClaimTime;
432
433 //attributes of actionautoConfirm
434 bool _isautoConfirmDone;
435 uint _autoConfirmTime;
436
437 uint _max;
438 bool _issellerDone;
439 uint _i = 0;
440
441 address[] _sellerAddress;
442 function sellerT(){
443 _max = now*1000;
444 }
445
446 function regist(address a) public {
447 _sellerAddress[_i] = a;
448 _i++;
449 }
450
451 function getAddress() public returns (address a){
452 return _sellerAddress[_i];
453 }
454
455 function createDone(address a){
456 _createTime = now;
457 _issellerDone = true;
458 }
459
460 function createTime() returns (uint result){
461 if(_iscreateDone){
462 return _createTime;
463 }
464 return _max;
465 }
466
467 function abortDone(address a){
468 _abortTime = now;
469 _issellerDone = true;
470 }
471
472 function abortTime() returns (uint result){
473 if(_isabortDone){
474 return _abortTime;
475 }
476 return _max;
477 }
478
479 function confirmClaimDone(address a){
480 _confirmClaimTime = now;
481 _issellerDone = true;
482 }
483
484 function confirmClaimTime() returns (uint result){
485 if(_isconfirmClaimDone){
486 return _confirmClaimTime;
487 }
488 return _max;
489 }
490
491 function autoConfirmDone(address a){
492 _autoConfirmTime = now;
493 _issellerDone = true;
494 }
495
496 function autoConfirmTime() returns (uint result){
497 if(_isautoConfirmDone){
498 return _autoConfirmTime;
499 }
500 return _max;
501 }
502
503 function contains(address a) returns (bool result) {
504 for (uint _j = 0; _j < _sellerAddress.length; _j++ ) { //for loop example
505 if (a == _sellerAddress[_j]){
506 return true;
507 }
508 }
509 return false;
510 }
511
512 }