ExampleofHouseLeasingContract
跳到导航
跳到搜索
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 }
1 /* Houselease.sol */
2 pragma solidity ^0.4.0;
3
4 import "./RenterT.sol";
5 import "./TenantT.sol";
6
7 contract Houselease {
8
9 RenterT Renter;
10 TenantT Tenant;
11
12 House house;
13 contractInfo infos;
14
15 uint start;
16 struct contractInfo{
17 uint renterBail;
18 uint tenantBail;
19 uint rental;
20 uint totalRental;
21 uint penalty;
22 uint startLeasingTime;
23 uint endLeasingTime;
24 uint payDate;
25 uint payDuration;
26 }
27 struct House{
28 uint ownershipNumber;
29 bytes32 location;
30 uint area;
31 bytes32 usage;
32 uint price;
33 uint useRight;
34 uint usufruct;
35 uint dispositionRight;
36 uint possessionRight;
37 }
38
39 function Houselease(){
40 start = now;
41 Renter = new RenterT();
42 Tenant = new TenantT();
43 }
44
45 modifier onlyRenter{
46 require(Renter.contains(msg.sender));
47 _;
48 }
49
50 modifier onlyTenant{
51 require(Tenant.contains(msg.sender));
52 _;
53 }
54
55 modifier term2Modifier{
56 require(now > Renter.registerHouseTime());
57 require(infos.tenantBail > 0);
58 _;
59 }
60
61 modifier term3Modifier{
62 require((now > Tenant.confirmLeaseTime()) &&(now < Tenant.confirmLeaseTime()+604800));
63 require(house.useRight > 0);
64 _;
65 }
66
67 modifier term4Modifier{
68 require(now < Tenant.confirmLeaseTime());
69 require(infos.rental > 0);
70 _;
71 }
72
73 modifier term6Modifier{
74 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+604800));
75 require(house.useRight > 0);
76 _;
77 }
78
79 modifier term7_1Modifier{
80 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+1296000));
81 _;
82 }
83
84 modifier term7_2Modifier{
85 require((now > Renter.checkHouseTime()) &&(now < Renter.checkHouseTime()+1296000));
86 _;
87 }
88
89 function registerHouse() onlyRenter() public payable {
90 //USER CODE HERE
91 //CHECK
92
93 }
94
95 function confirmLease(uint endLeasingDuration, uint payDuration) onlyTenant() term2Modifier() public payable {
96 //USER CODE HERE
97 infos.startLeasingTime = now;
98 infos.endLeasingTime = endLeasingDuration + now;
99 infos.payDate = payDuration + now;
100 infos.payDuration = payDuration;
101 //CHECK
102 assert(infos.startLeasingTime == now && (infos.endLeasingTime == endLeasingDuration + now && (infos.payDate == payDuration + now && infos.payDuration == payDuration)));
103 }
104
105 function transferHouse() onlyRenter() term3Modifier() public payable {
106 //USER CODE HERE
107 //CHECK
108
109 }
110
111 function payRent() onlyTenant() term4Modifier() public payable {
112 //USER CODE HERE
113 infos.payDate = infos.payDate + infos.payDuration;
114 infos.totalRental = infos.totalRental + infos.rental;
115 msg.sender.transfer(house.useRight);
116 //CHECK
117 assert(infos.payDate == infos.payDate + infos.payDuration && infos.totalRental == infos.totalRental + infos.rental);
118 }
119
120 function collectRent() onlyRenter() term7_1Modifier() public payable {
121 //USER CODE HERE
122 infos.totalRental = 0;
123 msg.sender.transfer(infos.totalRental);
124 //CHECK
125 assert(infos.totalRental == 0);
126 }
127
128 function returnHouse() onlyTenant() term6Modifier() public payable {
129 //USER CODE HERE
130 address(Renter).transfer(house.useRight);
131 //CHECK
132
133 }
134
135 }
1 /* RenterT.sol */
2 pragma solidity ^0.4.22;
3
4 contract RenterT{
5
6
7 //attributes of actionregisterHouse
8 bool _isregisterHouseDone;
9 uint _registerHouseTime;
10
11 //attributes of actioncollectRent
12 bool _iscollectRentDone;
13 uint _collectRentTime;
14
15 //attributes of actioncollectBail
16 bool _iscollectBailDone;
17 uint _collectBailTime;
18
19 //attributes of actiontransferHouse
20 bool _istransferHouseDone;
21 uint _transferHouseTime;
22
23 //attributes of actioncheckHouse
24 bool _ischeckHouseDone;
25 uint _checkHouseTime;
26
27 uint _max;
28 bool _isRenterDone;
29 uint _i;
30
31 address[] _RenterAddress;
32 function RenterT(){
33 _max = now*1000;
34 }
35
36 function regist(address a) public {
37 _RenterAddress[_i] = a;
38 _i++;
39 }
40
41 function getAddress(uint _i) public returns (address a){
42 return _RenterAddress[_i];
43 }
44
45 function registerHouseDone(address a){
46 _registerHouseTime = now;
47 _isRenterDone = true;
48 }
49
50 function registerHouseTime() returns (uint result){
51 if(_isregisterHouseDone){
52 return _registerHouseTime;
53 }
54 return _max;
55 }
56
57 function collectRentDone(address a){
58 _collectRentTime = now;
59 _isRenterDone = true;
60 }
61
62 function collectRentTime() returns (uint result){
63 if(_iscollectRentDone){
64 return _collectRentTime;
65 }
66 return _max;
67 }
68
69 function collectBailDone(address a){
70 _collectBailTime = now;
71 _isRenterDone = true;
72 }
73
74 function collectBailTime() returns (uint result){
75 if(_iscollectBailDone){
76 return _collectBailTime;
77 }
78 return _max;
79 }
80
81 function transferHouseDone(address a){
82 _transferHouseTime = now;
83 _isRenterDone = true;
84 }
85
86 function transferHouseTime() returns (uint result){
87 if(_istransferHouseDone){
88 return _transferHouseTime;
89 }
90 return _max;
91 }
92
93 function checkHouseDone(address a){
94 _checkHouseTime = now;
95 _isRenterDone = true;
96 }
97
98 function checkHouseTime() returns (uint result){
99 if(_ischeckHouseDone){
100 return _checkHouseTime;
101 }
102 return _max;
103 }
104
105 function contains(address a) returns (bool result) {
106 for (uint _j = 0; _j < _RenterAddress.length; _j++ ) { //for loop example
107 if (a == _RenterAddress[_j]){
108 return true;
109 }
110 }
111 return false;
112 }
113
114 }
1 /* TenantT.sol */
2 pragma solidity ^0.4.22;
3
4 contract TenantT{
5
6
7 //attributes of actionconfirmLease
8 bool _isconfirmLeaseDone;
9 uint _confirmLeaseTime;
10
11 //attributes of actionpayRent
12 bool _ispayRentDone;
13 uint _payRentTime;
14
15 //attributes of actionreturnHouse
16 bool _isreturnHouseDone;
17 uint _returnHouseTime;
18
19 //attributes of actioncollectBail
20 bool _iscollectBailDone;
21 uint _collectBailTime;
22
23 uint _max;
24 bool _isTenantDone;
25 uint _i;
26
27 address[] _TenantAddress;
28 function TenantT(){
29 _max = now*1000;
30 }
31
32 function regist(address a) public {
33 _TenantAddress[_i] = a;
34 _i++;
35 }
36
37 function getAddress(uint _i) public returns (address a){
38 return _TenantAddress[_i];
39 }
40
41 function confirmLeaseDone(address a){
42 _confirmLeaseTime = now;
43 _isTenantDone = true;
44 }
45
46 function confirmLeaseTime() returns (uint result){
47 if(_isconfirmLeaseDone){
48 return _confirmLeaseTime;
49 }
50 return _max;
51 }
52
53 function payRentDone(address a){
54 _payRentTime = now;
55 _isTenantDone = true;
56 }
57
58 function payRentTime() returns (uint result){
59 if(_ispayRentDone){
60 return _payRentTime;
61 }
62 return _max;
63 }
64
65 function returnHouseDone(address a){
66 _returnHouseTime = now;
67 _isTenantDone = true;
68 }
69
70 function returnHouseTime() returns (uint result){
71 if(_isreturnHouseDone){
72 return _returnHouseTime;
73 }
74 return _max;
75 }
76
77 function collectBailDone(address a){
78 _collectBailTime = now;
79 _isTenantDone = true;
80 }
81
82 function collectBailTime() returns (uint result){
83 if(_iscollectBailDone){
84 return _collectBailTime;
85 }
86 return _max;
87 }
88
89 function contains(address a) returns (bool result) {
90 for (uint _j = 0; _j < _TenantAddress.length; _j++ ) { //for loop example
91 if (a == _TenantAddress[_j]){
92 return true;
93 }
94 }
95 return false;
96 }
97
98 }