.. DO NOT EDIT. .. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY. .. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE: .. "api/gallery/contracts/verification/plot_03_design_by_contract.py" .. LINE NUMBERS ARE GIVEN BELOW. .. only:: html .. note:: :class: sphx-glr-download-link-note :ref:`Go to the end ` to download the full example code or to run this example in your browser via JupyterLite. .. rst-class:: sphx-glr-example-title .. _sphx_glr_api_gallery_contracts_verification_plot_03_design_by_contract.py: Meyer's design by contract: an escrow with checked clauses (1986) ================================================================= Bertrand Meyer's Eiffel treats every routine as a contract. The caller must establish the *precondition*; the routine then guarantees the *postcondition*; and every public routine preserves the class *invariant*. Checked at run time, a violated clause names the culprit: a failed precondition is the caller's bug, a failed postcondition or invariant the supplier's. In Hoare's notation, a routine ``r`` must satisfy .. math:: \{\mathrm{pre}_r \wedge \mathrm{INV}\}\; r\; \{\mathrm{post}_r \wedge \mathrm{INV}\}. Solidity's ``require`` and ``assert`` are the same idea, and a violated clause reverts the transaction. The escrow below holds deposits for several accounts; its invariant ties the recorded deposits to the ether it actually holds. A refund with a rounding bug is stopped by its postcondition, and a sweep that forgets to update the books is stopped by the invariant, each before any state changes. .. GENERATED FROM PYTHON SOURCE LINES 25-30 .. code-block:: Python import matplotlib.pyplot as plt import blockchainkit as bk from blockchainkit.contracts import Contract, ensures, requires .. GENERATED FROM PYTHON SOURCE LINES 31-33 An escrow with a precondition, a postcondition and an invariant --------------------------------------------------------------- .. GENERATED FROM PYTHON SOURCE LINES 33-108 .. code-block:: Python class Escrow(Contract): layout = ("deposits", "total", "fee") def receive(self): self.write("deposits", self.sender, self.read("deposits", self.sender) + self.value) self.write("total", self.read("total") + self.value) @requires( lambda self, amount: 0 < amount <= self.read("deposits", self.sender), "refund must be within your deposit", ) @ensures( lambda self, old, result, amount: ( self.read("deposits", self.sender) == old("deposits", self.sender) - amount ), "deposit not reduced by the refund", ) def refund(self, amount): fee = amount // 100 # A bug: the fee is charged to the depositor's record twice. self.write("deposits", self.sender, self.read("deposits", self.sender) - amount - fee) self.write("total", self.read("total") - amount) self.call(self.sender, None, value=amount) def sweep(self, to): self.call(to, None, value=self.ether_balance()) # Forgets to update the books. def invariant(self): return self.read("total") == self.ether_balance() == sum(self.entries("deposits").values()) world = bk.contracts.World() for account in ("alice", "bob"): world.fund(account, 1_000) escrow = world.deploy("operator", Escrow) world.transact("alice", escrow, value=500) world.transact("bob", escrow, value=300) attempts = { "refund 50": world.transact("alice", escrow, "refund", 50), "refund 600": world.transact("alice", escrow, "refund", 600), "refund 200": world.transact("alice", escrow, "refund", 200), "sweep": world.transact("mallory", escrow, "sweep", "mallory"), } for name, receipt in attempts.items(): print(f"{name:10s} ->", "ok" if receipt.success else receipt.error) assert attempts["refund 50"].success assert attempts["refund 600"].error == "refund must be within your deposit" assert attempts["refund 200"].error == "deposit not reduced by the refund" assert attempts["sweep"].error == "invariant of Escrow violated" assert world.balance(escrow) == 750 and world.balance("mallory") == 0 fig, ax = plt.subplots(figsize=(7, 3.5)) names = list(attempts) ax.barh( names, [1] * len(names), color=["#16a34a" if r.success else "#dc2626" for r in attempts.values()], ) for row, receipt in enumerate(attempts.values()): ax.text( 0.02, row, "succeeded" if receipt.success else receipt.error, va="center", color="white", fontsize=9, ) ax.set(xticks=[], title="Each clause stops a different fault") ax.invert_yaxis() fig.tight_layout() plt.show() .. image-sg:: /api/gallery/contracts/verification/images/sphx_glr_plot_03_design_by_contract_001.png :alt: Each clause stops a different fault :srcset: /api/gallery/contracts/verification/images/sphx_glr_plot_03_design_by_contract_001.png :class: sphx-glr-single-img .. rst-class:: sphx-glr-script-out .. code-block:: none refund 50 -> ok refund 600 -> refund must be within your deposit refund 200 -> deposit not reduced by the refund sweep -> invariant of Escrow violated .. GENERATED FROM PYTHON SOURCE LINES 109-114 Exercise -------- A refund of 50 passed although the code is buggy. For which amounts does the postcondition catch the fee bug, and why does that make run-time checking weaker than proof? .. rst-class:: sphx-glr-timing **Total running time of the script:** (0 minutes 0.033 seconds) .. _sphx_glr_download_api_gallery_contracts_verification_plot_03_design_by_contract.py: .. only:: html .. container:: sphx-glr-footer sphx-glr-footer-example .. container:: lite-badge .. image:: images/jupyterlite_badge_logo.svg :target: ../../../../lite/lab/index.html?path=api/gallery/contracts/verification/plot_03_design_by_contract.ipynb :alt: Launch JupyterLite :width: 150 px .. container:: sphx-glr-download sphx-glr-download-jupyter :download:`Download Jupyter notebook: plot_03_design_by_contract.ipynb ` .. container:: sphx-glr-download sphx-glr-download-python :download:`Download Python source code: plot_03_design_by_contract.py ` .. container:: sphx-glr-download sphx-glr-download-zip :download:`Download zipped: plot_03_design_by_contract.zip ` .. only:: html .. rst-class:: sphx-glr-signature `Gallery generated by Sphinx-Gallery `_