一笔设备租赁费用先被登记为一百二十元，核对后应为一百元。客户支付一百元，随后又获得二十五元折扣，最后收到二十五元退款。如果订单只有一个可修改的 amount 字段，最终的七十五元无法解释这些变化：最初登记了什么、客户付了多少、折扣是否已经退成现金，都要另找记录。

有效时间与记录时间保留了目录历史；费用记录还需要解释金额变化之间的关系。本篇使用合成租赁事实构造一个教学账本，检查费用、收款、折扣、退款和冲正。所有金额和处理规则都是实验输入，不代表真实支付，也不构成财务合规方案。

一笔费用涉及四种对象

费用事实表示“登记了一项应收一百元的费用”，它带有事实编号、币种、金额和发生时刻。账户提供累计变化的分类视角，分录记录某个账户的一次有符号变化，会计事务把相互对应的分录连接起来。四种对象的身份不同，不能都用订单编号替代。

本文引用 Martin Fowler 于2005年1月22日发布的两篇草稿。Accounting Entry 明确说明：原书把 Account 和 Entry 放在同一个模式中，网页草稿将它们分开讨论。因此这里的分篇术语来自2005年草稿，不把网页组织方式写成原书章节结构。Accounting Entry：How it Works

同日的 Accounting Transaction 草稿描述了连接两条或更多分录、使金额之和为零的事务。这个连接关系才是本实验采用的核心约束；具体租赁费用应进入哪些账户，仍需另行定义。Accounting Transaction

实验对象	保存的内容	不能据此推断的事
`fact`	已登记的费用、收款、折扣等事实	已经记账、外部付款已经完成
`account`	账户编号与单一币种	本身保存了全部业务过程
`entry`	所属账户及整数分变化	单独一条就完整解释了资金对应关系
`journal`	事实引用和成组分录的身份	数据库提交成功就保证业务正确

flowchart LR
  F[Fact 已登记的业务事实] -->|关联依据| J[Journal 会计事务]
  J -->|包含至少两条| E[Entry 有符号金额变化]
  E -->|归属一个| A[Account 单币种账户]
  E -->|按账户求和| B[Balance 派生余额]
  J -->|另加反向事务| R[Reversal 保留原事务]

图是实验关系的流程示意，不是会计科目图。实验先登记六个事实，此时查询分录仍为空。只有显式调用 post 才产生会计事务；将事实保存成功和记账完成分开观察，才能发现中间步骤是否遗漏。

金额和账户先限定到可检验的范围

账本只接受 CNY、USD 两种币种，输入必须能精确表示为整数分，绝对金额不超过十亿元。它用 Decimal 读取十进制文本，再检查有效小数位；不通过浮点数中转，也不在记账入口偷偷舍入。10.005、极长的小数尾数和非有限值都会被拒绝。币种相同仍不足以保证金额正确，但币种不同的数值不能直接抵消。

教学符号约定如下：应收账户 receivable 和现金账户 cash 的增加记正数，收入账户 revenue 的对应增加记负数。这样，每项费用可表示为应收增加和收入对应增加，账户余额则是该账户所有分录的有符号总和。这是为了检查关系而选择的表示法，不是完整借贷规则或通用科目表。

一百元费用产生 receivable +100、revenue -100。一百元收款产生 cash +100、receivable -100。两项事务分别平衡，合起来使应收余额归零、现金余额增加一百元。若直接把订单状态从“未支付”改为“已支付”，这些账户变化并不会因此自动存在。

post 检查至少两条非零分录、账户币种等于事实币种、各项合计为零、正项合计等于事实金额。最后一条是本实验增加的约束：它会拒绝用五十元的一对分录处理一百元事实。即便这些检查都通过，把费用配到错误的账户仍可能平衡；实验没有实现事实种类到允许账户组合的完整规则。

余额不单独作为可覆盖字段保存，而是按账户对分录求和。这样，显示的余额可以回到组成它的记录，冲正也不需要执行“把旧余额减回去”的隐藏修补。代价是查询要扫描相关分录；大规模系统可以考虑派生读模型，但必须保持它与原始记录的对应关系。这个小实验没有加入缓存，避免同时验证两套状态。

表结构里的外键检查引用是否存在，主键检查事务内分录序号是否重复，它们都不理解“费用应该如何记账”。将约束逐条定位到数据库或应用层，有助于解释绕过入口会失去哪些保证。尤其不能因为表名叫账本、分录字段不可修改，就推断其余额一定正确。

更正、折扣和退款留下不同记录

最初的费用事实 F1 为一百二十元，事务 T1 增加同额应收。发现金额错误后，实验追加 T1-R，逐条复制 T1 的账户并反转符号，再以新事实 F2 登记正确的一百元费用。T1 的原始分录仍然存在，T1 与 T1-R 的账户影响相互抵消。

直接把一百二十改成一百会丢失更正依据；额外加一个负二十元也只有在明确采用差额调整政策时才有充分含义。本实验选择全额冲正后重新入账，冲正事务保存原事务引用，唯一约束禁止同一原事务被再次全额冲正。这只是当前教学策略，并未实现部分冲正或多次差额调整。

事务	事实或原因	分录，金额单位为元
T1	原费用120	应收 +120；收入 -120
T1-R	冲正 T1	应收 -120；收入 +120
T2	正确费用100	应收 +100；收入 -100
T3	收款100	现金 +100；应收 -100
T4	收款后折扣25	收入 +25；应收 -25
T5	实际登记退款25	应收 +25；现金 -25

折扣和退款之间存在可观察的中间状态。T4 后，现金仍为一百元，应收为负二十五元，收入为负七十五元。负应收在这个简化模型里表示应返还的余额；更复杂的模型可以另设退款义务账户，但不能靠改名省略真实的转账事实。

T5 之后，现金为七十五元，应收归零，收入为负七十五元。折扣降低本例确认的费用，退款减少现金，两者不会因为金额相同而成为同一动作。实验分别断言折扣后的中间余额和退款后的最终余额，避免只看最后总数而漏掉过程错误。

租赁取消也不能直接等同于退款。前文取消释放设备时段，是否调整费用要看收费约定。产生退款义务之后，还需单独确认现金是否退回。因此本例将退款作为单独夹具输入，没有给 cancel 偷加账本副作用，也没有根据资源已经空闲推断资金已经退还。

SQLite 触发器拒绝已存事实、事务头和分录的更新、删除；更正只能追加。这是本实验的存储选择。来源草稿也讨论了“始终不可改”和“入账后不可改”的不同选择，不能把本例限制扩写成所有系统都必须采用的方案。只禁止修改也不等于防篡改：直接插入、授权控制和外部事实真实性仍在边界之外。

会计事务和数据库事务分别验证

会计事务回答一组分录是否满足账本约束，数据库事务回答这次写入是否作为一个整体提交。两个概念在代码里相遇，但证明方法不同。post 先在应用层验证金额关系，再用 SQLite 事务写入事务头和各条分录。

第一个反例输入 +100 与 -99，应用检查以 unbalanced journal 拒绝，数据库中原有分录不变。第二个反例把 USD 现金账户与 CNY 收入账户配成数值上相反的一对，仍因币种不同而拒绝。单条分录、事实金额不符、重复事务编号，也各有独立断言。

随后在写完第一条分录后主动抛出异常。查询证实新事务头不存在，旧分录集合完全未变。这证明本次进程内、同一连接的 SQLite 写入整体回滚，不是在失败后仅删除某一条记录。实验使用内存数据库，没有测试进程崩溃后的磁盘恢复。

最后另建一个独立账本，绕过 post，直接在数据库事务里插入一个事务头和一条一百元分录。数据库成功提交，查询合计得到一万分。原子提交并不检查这组分录必须有两条、合计必须为零；这些跨行约束在本实验中由应用入口负责。这个故意保留的反例界定了实现保证，不能把它包装成可让任意写入者使用的完整账本服务。

运行和阅读结果

代码、表结构、模型图与原始输出放在第13篇实验包。解压后，从包含 examples 的目录执行：

1	`bash examples/software-modeling/labs/13/run.sh`

入口只依赖 Python 标准库，实际运行环境是 Python 3.14.4、SQLite 3.51.3。脚本逐条比较余额、原始分录与异常类别，预期异常打印 REJECT；未拒绝错误输入或结果不符会抛出断言并以非零码退出。全部场景通过时退出码为零。

PASS final_balances_minor actual={'cash': 7500, 'receivable': 0, 'revenue': -7500}
REJECT unbalanced ValueError: unbalanced journal
PASS database_rollback_header actual=0
PASS db_commit_can_be_unbalanced actual=10000
PASS 13: 23 scenarios; accounting_validation != database_atomicity

完整记录位于 examples/software-modeling/evidence/13/output.txt，边界说明位于 examples/software-modeling/models/13/semantics.md。记录中的数字是断言读取的实际值，不是示意日志；最后一项不平衡提交是刻意构造的反例。

本篇账本是独立候选实验，没有修改前文 Java 租赁基线的预留、取消和重试契约。账本重复事务编号直接报错，并未实现同编号同负载重放；同一事实也可能被不同事务重复引用，因此不能把主键唯一称为业务幂等。要接到租赁请求链路，还需定义事实去重、允许的入账组合、支付确认来源与对账方式。当前可核对的是这组明确给定的费用变化，以及应用校验与存储原子性各自覆盖的范围。