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.

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.

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 <br>
 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 <br>
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 <br>
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.