﻿<?xml version="1.0"?>
<feed xmlns="http://www.w3.org/2005/Atom" xml:lang="zh-Hans-CN">
	<id>https://www.smartlegalcontract.cn/mediawiki/index.php?action=history&amp;feed=atom&amp;title=ExampleofHouseLeasingContract</id>
	<title>ExampleofHouseLeasingContract - 版本历史</title>
	<link rel="self" type="application/atom+xml" href="https://www.smartlegalcontract.cn/mediawiki/index.php?action=history&amp;feed=atom&amp;title=ExampleofHouseLeasingContract"/>
	<link rel="alternate" type="text/html" href="https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;action=history"/>
	<updated>2026-05-13T14:30:20Z</updated>
	<subtitle>本wiki的该页面的版本历史</subtitle>
	<generator>MediaWiki 1.35.0</generator>
	<entry>
		<id>https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=515&amp;oldid=prev</id>
		<title>20201027：/*  House-leasing contract  */</title>
		<link rel="alternate" type="text/html" href="https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=515&amp;oldid=prev"/>
		<updated>2021-09-12T08:05:50Z</updated>

		<summary type="html">&lt;p&gt;&lt;span dir=&quot;auto&quot;&gt;&lt;span class=&quot;autocomment&quot;&gt;House-leasing contract&lt;/span&gt;&lt;/span&gt;&lt;/p&gt;
&lt;a href=&quot;https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;amp;diff=515&amp;amp;oldid=462&quot;&gt;显示更改&lt;/a&gt;</summary>
		<author><name>20201027</name></author>
	</entry>
	<entry>
		<id>https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=462&amp;oldid=prev</id>
		<title>2021年3月13日 (六) 03:59 20201027</title>
		<link rel="alternate" type="text/html" href="https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=462&amp;oldid=prev"/>
		<updated>2021-03-13T03:59:30Z</updated>

		<summary type="html">&lt;p&gt;&lt;/p&gt;
&lt;table class=&quot;diff diff-contentalign-left diff-editfont-monospace&quot; data-mw=&quot;interface&quot;&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;tr class=&quot;diff-title&quot; lang=&quot;zh-Hans-CN&quot;&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;←上一版本&lt;/td&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;2021年3月13日 (六) 03:59的版本&lt;/td&gt;
				&lt;/tr&gt;&lt;tr&gt;&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot; id=&quot;mw-diff-left-l1&quot; &gt;第1行：&lt;/td&gt;
&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot;&gt;第1行：&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}}&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}}&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt;−&lt;/td&gt;&lt;td style=&quot;color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;&lt;del style=&quot;font-weight: bold; text-decoration: none;&quot;&gt;__NOEDITSECTION__&lt;/del&gt;&lt;/div&gt;&lt;/td&gt;&lt;td colspan=&quot;2&quot;&gt; &lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;=== &amp;lt;div style=&amp;quot; background:#EBEBEB; padding-top: 10px; height:45px; padding-left:15px &amp;quot;&amp;gt; House-leasing contract &amp;lt;/div&amp;gt; ===&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;=== &amp;lt;div style=&amp;quot; background:#EBEBEB; padding-top: 10px; height:45px; padding-left:15px &amp;quot;&amp;gt; House-leasing contract &amp;lt;/div&amp;gt; ===&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{| class=&amp;quot;wikitable&amp;quot;&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{| class=&amp;quot;wikitable&amp;quot;&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;/table&gt;</summary>
		<author><name>20201027</name></author>
	</entry>
	<entry>
		<id>https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=461&amp;oldid=prev</id>
		<title>2021年3月13日 (六) 03:59 20201027</title>
		<link rel="alternate" type="text/html" href="https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=461&amp;oldid=prev"/>
		<updated>2021-03-13T03:59:14Z</updated>

		<summary type="html">&lt;p&gt;&lt;/p&gt;
&lt;table class=&quot;diff diff-contentalign-left diff-editfont-monospace&quot; data-mw=&quot;interface&quot;&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;col class=&quot;diff-marker&quot; /&gt;
				&lt;col class=&quot;diff-content&quot; /&gt;
				&lt;tr class=&quot;diff-title&quot; lang=&quot;zh-Hans-CN&quot;&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;←上一版本&lt;/td&gt;
				&lt;td colspan=&quot;2&quot; style=&quot;background-color: #fff; color: #202122; text-align: center;&quot;&gt;2021年3月13日 (六) 03:59的版本&lt;/td&gt;
				&lt;/tr&gt;&lt;tr&gt;&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot; id=&quot;mw-diff-left-l1&quot; &gt;第1行：&lt;/td&gt;
&lt;td colspan=&quot;2&quot; class=&quot;diff-lineno&quot;&gt;第1行：&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}}&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}}&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td colspan=&quot;2&quot;&gt; &lt;/td&gt;&lt;td class='diff-marker'&gt;+&lt;/td&gt;&lt;td style=&quot;color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;&lt;ins style=&quot;font-weight: bold; text-decoration: none;&quot;&gt;__NOEDITSECTION__&lt;/ins&gt;&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;=== &amp;lt;div style=&amp;quot; background:#EBEBEB; padding-top: 10px; height:45px; padding-left:15px &amp;quot;&amp;gt; House-leasing contract &amp;lt;/div&amp;gt; ===&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;=== &amp;lt;div style=&amp;quot; background:#EBEBEB; padding-top: 10px; height:45px; padding-left:15px &amp;quot;&amp;gt; House-leasing contract &amp;lt;/div&amp;gt; ===&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;tr&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{| class=&amp;quot;wikitable&amp;quot;&lt;/div&gt;&lt;/td&gt;&lt;td class='diff-marker'&gt; &lt;/td&gt;&lt;td style=&quot;background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;&quot;&gt;&lt;div&gt;{| class=&amp;quot;wikitable&amp;quot;&lt;/div&gt;&lt;/td&gt;&lt;/tr&gt;
&lt;/table&gt;</summary>
		<author><name>20201027</name></author>
	</entry>
	<entry>
		<id>https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=402&amp;oldid=prev</id>
		<title>20201027：建立内容为“{{DISPLAYTITLE:&lt;span style=&quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&quot;&gt;{{FULLPAGENAME}}&lt;/span&gt;}} === &lt;div style=&quot; backgroun…”的新页面</title>
		<link rel="alternate" type="text/html" href="https://www.smartlegalcontract.cn/mediawiki/index.php?title=ExampleofHouseLeasingContract&amp;diff=402&amp;oldid=prev"/>
		<updated>2021-03-09T13:52:45Z</updated>

		<summary type="html">&lt;p&gt;建立内容为“{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}} === &amp;lt;div style=&amp;quot; backgroun…”的新页面&lt;/p&gt;
&lt;p&gt;&lt;b&gt;新页面&lt;/b&gt;&lt;/p&gt;&lt;div&gt;{{DISPLAYTITLE:&amp;lt;span style=&amp;quot;position: absolute; clip: rect(1px 1px 1px 1px); clip: rect(1px, 1px, 1px, 1px);&amp;quot;&amp;gt;{{FULLPAGENAME}}&amp;lt;/span&amp;gt;}}&lt;br /&gt;
=== &amp;lt;div style=&amp;quot; background:#EBEBEB; padding-top: 10px; height:45px; padding-left:15px &amp;quot;&amp;gt; House-leasing contract &amp;lt;/div&amp;gt; ===&lt;br /&gt;
{| class=&amp;quot;wikitable&amp;quot;&lt;br /&gt;
||&amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;House-leasing contract, takes assets as the transaction subject between lessor and lessee. There are 7 terms in the contract, including two aspects:&amp;lt;br&amp;gt; &amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;1) the lessor can register the house after depositing the rental deposit, and &amp;lt;br&amp;gt;&amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;&amp;amp;nbsp;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.&lt;br /&gt;
|}&lt;br /&gt;
'''&amp;lt;syntaxhighlight lang=&amp;quot;spec&amp;quot; line=&amp;quot;1&amp;quot;&amp;gt;&lt;br /&gt;
// HouseLease.scs&lt;br /&gt;
contract Houselease{&lt;br /&gt;
	party Renter{&lt;br /&gt;
		registerHouse()&lt;br /&gt;
		collectRent()&lt;br /&gt;
		collectBail()&lt;br /&gt;
		transferHouse()&lt;br /&gt;
		checkHouse()&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	party Tenant{&lt;br /&gt;
		confirmLease(endLeasingDuration:Date,&lt;br /&gt;
			payDuration:Date)&lt;br /&gt;
		payRent()&lt;br /&gt;
		returnHouse()&lt;br /&gt;
		collectBail()&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	house : House&lt;br /&gt;
	infos : contractInfo&lt;br /&gt;
	&lt;br /&gt;
	term term1 : Renter can registerHouse&lt;br /&gt;
		while deposit $infos::renterBail.&lt;br /&gt;
		&lt;br /&gt;
	term term2 : Tenant can confirmLease&lt;br /&gt;
		when after Renter did registerHouse&lt;br /&gt;
		while deposit $infos::tenantBail&lt;br /&gt;
		where infos::startLeasingTime = now and&lt;br /&gt;
			infos::endLeasingTime = endLeasingDuration + now&lt;br /&gt;
			and infos::payDate = payDuration + now&lt;br /&gt;
			and infos::payDuration = payDuration.&lt;br /&gt;
			&lt;br /&gt;
	term term3 : Renter must transferHouse&lt;br /&gt;
		when within 7 day after Tenant did confirmLease&lt;br /&gt;
		while deposit $ house::useRight.&lt;br /&gt;
	&lt;br /&gt;
	term term4 : Tenant must payRent&lt;br /&gt;
		when before Tenant did confirmLease		&lt;br /&gt;
		while deposit $infos::rental&lt;br /&gt;
			withdraw $house::useRight&lt;br /&gt;
		where infos::payDate = infos::payDate + infos::payDuration&lt;br /&gt;
			and infos::totalRental = infos::totalRental + infos::rental.&lt;br /&gt;
	&lt;br /&gt;
	term term5 : Renter can collectRent&lt;br /&gt;
		while withdraw $infos::totalRental&lt;br /&gt;
		where infos::totalRental = 0.&lt;br /&gt;
	&lt;br /&gt;
	term term6 : Tenant must returnHouse&lt;br /&gt;
		when within 7 day after Renter did checkHouse&lt;br /&gt;
		while deposit $house::useRight&lt;br /&gt;
			transfer $house::useRight to Renter.&lt;br /&gt;
	&lt;br /&gt;
	term term7_1 : Renter can collectBail&lt;br /&gt;
		when within 15 day after Renter did checkHouse&lt;br /&gt;
		while withdraw $infos::renterBail.&lt;br /&gt;
	&lt;br /&gt;
	term term7_2 : Tenant can collectBail&lt;br /&gt;
		when within 15 day after Renter did checkHouse&lt;br /&gt;
		while withdraw $infos::tenantBail.&lt;br /&gt;
		&lt;br /&gt;
		type contractInfo {&lt;br /&gt;
			renterBail : Money&lt;br /&gt;
			tenantBail : Money&lt;br /&gt;
			rental : Money&lt;br /&gt;
			totalRental : Money&lt;br /&gt;
			penalty : Money&lt;br /&gt;
			startLeasingTime : Date&lt;br /&gt;
			endLeasingTime : Date&lt;br /&gt;
			payDate : Date&lt;br /&gt;
			payDuration : Date&lt;br /&gt;
		}&lt;br /&gt;
		&lt;br /&gt;
		type House {&lt;br /&gt;
			ownershipNumber : integer&lt;br /&gt;
			location : String&lt;br /&gt;
			area : integer&lt;br /&gt;
			usage : String&lt;br /&gt;
			price : Money&lt;br /&gt;
			useRight : String&lt;br /&gt;
			usufruct : String&lt;br /&gt;
			dispositionRight : String&lt;br /&gt;
			possessionRight : String&lt;br /&gt;
		}&lt;br /&gt;
}&lt;br /&gt;
&amp;lt;/syntaxhighlight&amp;gt;'''&lt;br /&gt;
'''&amp;lt;syntaxhighlight lang=&amp;quot;spec&amp;quot; line=&amp;quot;1&amp;quot;&amp;gt;&lt;br /&gt;
/* Houselease.sol */&lt;br /&gt;
pragma solidity ^0.4.0;&lt;br /&gt;
		&lt;br /&gt;
import &amp;quot;./RenterT.sol&amp;quot;;&lt;br /&gt;
import &amp;quot;./TenantT.sol&amp;quot;;&lt;br /&gt;
&lt;br /&gt;
contract Houselease {&lt;br /&gt;
	&lt;br /&gt;
	RenterT Renter;&lt;br /&gt;
	TenantT Tenant;&lt;br /&gt;
	&lt;br /&gt;
	House house;&lt;br /&gt;
	contractInfo infos;&lt;br /&gt;
	&lt;br /&gt;
	uint start;&lt;br /&gt;
	struct contractInfo{&lt;br /&gt;
		uint renterBail;&lt;br /&gt;
		uint tenantBail;&lt;br /&gt;
		uint rental;&lt;br /&gt;
		uint totalRental;&lt;br /&gt;
		uint penalty;&lt;br /&gt;
		uint startLeasingTime;&lt;br /&gt;
		uint endLeasingTime;&lt;br /&gt;
		uint payDate;&lt;br /&gt;
		uint payDuration;&lt;br /&gt;
	}&lt;br /&gt;
	struct House{&lt;br /&gt;
		uint ownershipNumber;&lt;br /&gt;
		bytes32 location;&lt;br /&gt;
		uint area;&lt;br /&gt;
		bytes32 usage;&lt;br /&gt;
		uint price;&lt;br /&gt;
		uint useRight;&lt;br /&gt;
		uint usufruct;&lt;br /&gt;
		uint dispositionRight;&lt;br /&gt;
		uint possessionRight;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function Houselease(){&lt;br /&gt;
		start = now;&lt;br /&gt;
		Renter = new RenterT();&lt;br /&gt;
		Tenant = new TenantT();&lt;br /&gt;
	}&lt;br /&gt;
&lt;br /&gt;
	modifier onlyRenter{&lt;br /&gt;
		require(Renter.contains(msg.sender));&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier onlyTenant{&lt;br /&gt;
		require(Tenant.contains(msg.sender));&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term2Modifier{&lt;br /&gt;
		require(now &amp;gt; Renter.registerHouseTime());&lt;br /&gt;
		require(infos.tenantBail &amp;gt; 0);&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term3Modifier{&lt;br /&gt;
		require((now &amp;gt; Tenant.confirmLeaseTime()) &amp;amp;&amp;amp;(now &amp;lt; Tenant.confirmLeaseTime()+604800));&lt;br /&gt;
		require(house.useRight &amp;gt; 0);&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term4Modifier{&lt;br /&gt;
		require(now &amp;lt; Tenant.confirmLeaseTime());&lt;br /&gt;
		require(infos.rental &amp;gt; 0);&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term6Modifier{&lt;br /&gt;
		require((now &amp;gt; Renter.checkHouseTime()) &amp;amp;&amp;amp;(now &amp;lt; Renter.checkHouseTime()+604800));&lt;br /&gt;
		require(house.useRight &amp;gt; 0);&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term7_1Modifier{&lt;br /&gt;
		require((now &amp;gt; Renter.checkHouseTime()) &amp;amp;&amp;amp;(now &amp;lt; Renter.checkHouseTime()+1296000));&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	modifier term7_2Modifier{&lt;br /&gt;
		require((now &amp;gt; Renter.checkHouseTime()) &amp;amp;&amp;amp;(now &amp;lt; Renter.checkHouseTime()+1296000));&lt;br /&gt;
		_;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function registerHouse() onlyRenter() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		//CHECK&lt;br /&gt;
	&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function confirmLease(uint endLeasingDuration, uint payDuration) onlyTenant() term2Modifier() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		infos.startLeasingTime = now;&lt;br /&gt;
		infos.endLeasingTime = endLeasingDuration + now;&lt;br /&gt;
		infos.payDate = payDuration + now;&lt;br /&gt;
		infos.payDuration = payDuration;&lt;br /&gt;
		//CHECK&lt;br /&gt;
		assert(infos.startLeasingTime == now &amp;amp;&amp;amp; (infos.endLeasingTime == endLeasingDuration + now &amp;amp;&amp;amp; (infos.payDate == payDuration + now &amp;amp;&amp;amp; infos.payDuration == payDuration)));&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function transferHouse() onlyRenter() term3Modifier() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		//CHECK&lt;br /&gt;
	&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function payRent() onlyTenant() term4Modifier() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		infos.payDate = infos.payDate + infos.payDuration;&lt;br /&gt;
		infos.totalRental = infos.totalRental + infos.rental;&lt;br /&gt;
		msg.sender.transfer(house.useRight);&lt;br /&gt;
		//CHECK&lt;br /&gt;
		assert(infos.payDate == infos.payDate + infos.payDuration &amp;amp;&amp;amp; infos.totalRental == infos.totalRental + infos.rental);&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectRent() onlyRenter() term7_1Modifier() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		infos.totalRental = 0;&lt;br /&gt;
		msg.sender.transfer(infos.totalRental);&lt;br /&gt;
		//CHECK&lt;br /&gt;
		assert(infos.totalRental == 0);&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function returnHouse() onlyTenant() term6Modifier() public payable {&lt;br /&gt;
		//USER CODE HERE&lt;br /&gt;
		address(Renter).transfer(house.useRight);&lt;br /&gt;
		//CHECK&lt;br /&gt;
	&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
}&lt;br /&gt;
&amp;lt;/syntaxhighlight&amp;gt;'''&lt;br /&gt;
'''&amp;lt;syntaxhighlight lang=&amp;quot;spec&amp;quot; line=&amp;quot;1&amp;quot;&amp;gt;&lt;br /&gt;
/* RenterT.sol */&lt;br /&gt;
pragma solidity ^0.4.22;&lt;br /&gt;
&lt;br /&gt;
contract RenterT{&lt;br /&gt;
	&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actionregisterHouse&lt;br /&gt;
	bool _isregisterHouseDone;&lt;br /&gt;
	uint _registerHouseTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actioncollectRent&lt;br /&gt;
	bool _iscollectRentDone;&lt;br /&gt;
	uint _collectRentTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actioncollectBail&lt;br /&gt;
	bool _iscollectBailDone;&lt;br /&gt;
	uint _collectBailTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actiontransferHouse&lt;br /&gt;
	bool _istransferHouseDone;&lt;br /&gt;
	uint _transferHouseTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actioncheckHouse&lt;br /&gt;
	bool _ischeckHouseDone;&lt;br /&gt;
	uint _checkHouseTime;&lt;br /&gt;
	&lt;br /&gt;
	uint _max;&lt;br /&gt;
	bool _isRenterDone;&lt;br /&gt;
	uint _i;&lt;br /&gt;
	&lt;br /&gt;
	address[] _RenterAddress;&lt;br /&gt;
	function RenterT(){&lt;br /&gt;
		_max = now*1000;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function regist(address a) public {&lt;br /&gt;
		_RenterAddress[_i] = a;&lt;br /&gt;
		_i++;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function getAddress(uint _i) public returns (address a){&lt;br /&gt;
		return _RenterAddress[_i];&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function registerHouseDone(address a){&lt;br /&gt;
		_registerHouseTime = now;&lt;br /&gt;
		_isRenterDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function registerHouseTime() returns (uint result){&lt;br /&gt;
	    if(_isregisterHouseDone){&lt;br /&gt;
	        return _registerHouseTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectRentDone(address a){&lt;br /&gt;
		_collectRentTime = now;&lt;br /&gt;
		_isRenterDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectRentTime() returns (uint result){&lt;br /&gt;
	    if(_iscollectRentDone){&lt;br /&gt;
	        return _collectRentTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectBailDone(address a){&lt;br /&gt;
		_collectBailTime = now;&lt;br /&gt;
		_isRenterDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectBailTime() returns (uint result){&lt;br /&gt;
	    if(_iscollectBailDone){&lt;br /&gt;
	        return _collectBailTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function transferHouseDone(address a){&lt;br /&gt;
		_transferHouseTime = now;&lt;br /&gt;
		_isRenterDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function transferHouseTime() returns (uint result){&lt;br /&gt;
	    if(_istransferHouseDone){&lt;br /&gt;
	        return _transferHouseTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function checkHouseDone(address a){&lt;br /&gt;
		_checkHouseTime = now;&lt;br /&gt;
		_isRenterDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function checkHouseTime() returns (uint result){&lt;br /&gt;
	    if(_ischeckHouseDone){&lt;br /&gt;
	        return _checkHouseTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function contains(address a) returns (bool result) {&lt;br /&gt;
	    for (uint _j = 0; _j &amp;lt; _RenterAddress.length; _j++ ) {  //for loop example&lt;br /&gt;
            if (a == _RenterAddress[_j]){&lt;br /&gt;
                return true;&lt;br /&gt;
            }         &lt;br /&gt;
      }&lt;br /&gt;
      return false;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
}&lt;br /&gt;
&amp;lt;/syntaxhighlight&amp;gt;'''&lt;br /&gt;
'''&amp;lt;syntaxhighlight lang=&amp;quot;spec&amp;quot; line=&amp;quot;1&amp;quot;&amp;gt;&lt;br /&gt;
/* TenantT.sol */&lt;br /&gt;
pragma solidity ^0.4.22;&lt;br /&gt;
&lt;br /&gt;
contract TenantT{&lt;br /&gt;
	&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actionconfirmLease&lt;br /&gt;
	bool _isconfirmLeaseDone;&lt;br /&gt;
	uint _confirmLeaseTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actionpayRent&lt;br /&gt;
	bool _ispayRentDone;&lt;br /&gt;
	uint _payRentTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actionreturnHouse&lt;br /&gt;
	bool _isreturnHouseDone;&lt;br /&gt;
	uint _returnHouseTime;&lt;br /&gt;
	&lt;br /&gt;
	//attributes of actioncollectBail&lt;br /&gt;
	bool _iscollectBailDone;&lt;br /&gt;
	uint _collectBailTime;&lt;br /&gt;
	&lt;br /&gt;
	uint _max;&lt;br /&gt;
	bool _isTenantDone;&lt;br /&gt;
	uint _i;&lt;br /&gt;
	&lt;br /&gt;
	address[] _TenantAddress;&lt;br /&gt;
	function TenantT(){&lt;br /&gt;
		_max = now*1000;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function regist(address a) public {&lt;br /&gt;
		_TenantAddress[_i] = a;&lt;br /&gt;
		_i++;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function getAddress(uint _i) public returns (address a){&lt;br /&gt;
		return _TenantAddress[_i];&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function confirmLeaseDone(address a){&lt;br /&gt;
		_confirmLeaseTime = now;&lt;br /&gt;
		_isTenantDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function confirmLeaseTime() returns (uint result){&lt;br /&gt;
	    if(_isconfirmLeaseDone){&lt;br /&gt;
	        return _confirmLeaseTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function payRentDone(address a){&lt;br /&gt;
		_payRentTime = now;&lt;br /&gt;
		_isTenantDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function payRentTime() returns (uint result){&lt;br /&gt;
	    if(_ispayRentDone){&lt;br /&gt;
	        return _payRentTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function returnHouseDone(address a){&lt;br /&gt;
		_returnHouseTime = now;&lt;br /&gt;
		_isTenantDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function returnHouseTime() returns (uint result){&lt;br /&gt;
	    if(_isreturnHouseDone){&lt;br /&gt;
	        return _returnHouseTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectBailDone(address a){&lt;br /&gt;
		_collectBailTime = now;&lt;br /&gt;
		_isTenantDone = true;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function collectBailTime() returns (uint result){&lt;br /&gt;
	    if(_iscollectBailDone){&lt;br /&gt;
	        return _collectBailTime;&lt;br /&gt;
	    }&lt;br /&gt;
	    return _max;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
	function contains(address a) returns (bool result) {&lt;br /&gt;
	    for (uint _j = 0; _j &amp;lt; _TenantAddress.length; _j++ ) {  //for loop example&lt;br /&gt;
            if (a == _TenantAddress[_j]){&lt;br /&gt;
                return true;&lt;br /&gt;
            }         &lt;br /&gt;
      }&lt;br /&gt;
      return false;&lt;br /&gt;
	}&lt;br /&gt;
	&lt;br /&gt;
}&lt;br /&gt;
&amp;lt;/syntaxhighlight&amp;gt;'''&lt;/div&gt;</summary>
		<author><name>20201027</name></author>
	</entry>
</feed>