.. DO NOT EDIT. .. THIS FILE WAS AUTOMATICALLY GENERATED BY SPHINX-GALLERY. .. TO MAKE CHANGES, EDIT THE SOURCE PYTHON FILE: .. "api/gallery/contracts/verification/plot_01_floyd_hoare.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_01_floyd_hoare.py: Floyd and Hoare: proving a withdrawal correct with assertions (1967-1969) ========================================================================= Floyd attached an assertion to every arrow of a flowchart and asked that each instruction carry a true assertion to a true one. Hoare compressed the idea into the triple :math:`\{P\}\,S\,\{Q\}`: if P holds before S runs and S finishes, Q holds afterwards. The rule for an assignment runs backwards, .. math:: \{Q[e/x]\}\; x := e\; \{Q\}, so a postcondition can be pushed back through the code until it becomes a condition on the inputs, the *weakest precondition*. Proving the triple then means showing that P implies it. The program below withdraws from a balance and credits the receiver. The property to prove is conservation: the balance plus what was received never changes. With unbounded integers the weakest precondition reduces to the property itself, so it holds; with 4-bit words, a credit that wraps around breaks a different property, and a check over every state finds the counterexample. .. GENERATED FROM PYTHON SOURCE LINES 27-33 .. code-block:: Python import itertools import matplotlib.pyplot as plt import blockchainkit as bk .. GENERATED FROM PYTHON SOURCE LINES 34-36 The weakest precondition of conservation ---------------------------------------- .. GENERATED FROM PYTHON SOURCE LINES 36-58 .. code-block:: Python withdraw = """ require(amount <= balance) balance = balance - amount received = received + amount """ conservation = "balance + received == total" wp = bk.contracts.weakest_precondition(withdraw, conservation) print("wp =", bk.contracts.to_source(wp)) domain = {name: range(8) for name in ("balance", "amount", "received")} domain["total"] = range(16) result = bk.contracts.check_triple(conservation, withdraw, conservation, domain) print(result) assert result.holds and result.checked > 0 # P implies the weakest precondition in every state: the two checks agree. for values in itertools.product(*domain.values()): env = dict(zip(domain, values, strict=True)) if bk.contracts.evaluate(bk.contracts.parse_expression(conservation), env): assert bk.contracts.evaluate(wp, env) .. rst-class:: sphx-glr-script-out .. code-block:: none wp = not amount <= balance or balance - amount + (received + amount) == total TripleResult(holds=True, checked=512, counterexample=None) .. GENERATED FROM PYTHON SOURCE LINES 59-63 Wrapping words break "the receiver never loses" ----------------------------------------------- The receiver should end with at least the amount. With 4-bit words a large credit wraps around to a small number. .. GENERATED FROM PYTHON SOURCE LINES 63-90 .. code-block:: Python gains = "received >= amount" bits = 4 small = {name: range(2**bits) for name in ("balance", "amount", "received")} unbounded = bk.contracts.check_triple("1", withdraw, gains, small) wrapped = bk.contracts.check_triple("1", withdraw, gains, small, modulus=2**bits) print("unbounded:", unbounded.holds, " 4-bit words:", wrapped.counterexample) assert unbounded.holds and not wrapped.holds grid = [[0] * 2**bits for _ in range(2**bits)] for received, amount in itertools.product(range(2**bits), repeat=2): env = {"balance": 15, "amount": amount, "received": received} _, final = bk.contracts.run_program(withdraw, env, modulus=2**bits) grid[received][amount] = int(final["received"] < amount) fig, ax = plt.subplots(figsize=(5.5, 4.5)) image = ax.imshow(grid, origin="lower", cmap="Reds") ax.set( xlabel="amount", ylabel="received before", title="Where the postcondition fails (4-bit words)", ) fig.colorbar(image, ax=ax, label="1 = receiver ends below the amount") fig.tight_layout() plt.show() .. image-sg:: /api/gallery/contracts/verification/images/sphx_glr_plot_01_floyd_hoare_001.png :alt: Where the postcondition fails (4-bit words) :srcset: /api/gallery/contracts/verification/images/sphx_glr_plot_01_floyd_hoare_001.png :class: sphx-glr-single-img .. rst-class:: sphx-glr-script-out .. code-block:: none unbounded: True 4-bit words: {'amount': 1, 'balance': 1, 'received': 15} .. GENERATED FROM PYTHON SOURCE LINES 91-97 Exercise -------- Compute ``weakest_precondition(withdraw, "balance >= 0")``. Which part of it does the ``require`` contribute, and what happens to the result if you delete the ``require`` line? A worked solution is in :doc:`/exercises/contracts`. .. rst-class:: sphx-glr-timing **Total running time of the script:** (0 minutes 0.105 seconds) .. _sphx_glr_download_api_gallery_contracts_verification_plot_01_floyd_hoare.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_01_floyd_hoare.ipynb :alt: Launch JupyterLite :width: 150 px .. container:: sphx-glr-download sphx-glr-download-jupyter :download:`Download Jupyter notebook: plot_01_floyd_hoare.ipynb ` .. container:: sphx-glr-download sphx-glr-download-python :download:`Download Python source code: plot_01_floyd_hoare.py ` .. container:: sphx-glr-download sphx-glr-download-zip :download:`Download zipped: plot_01_floyd_hoare.zip ` .. only:: html .. rst-class:: sphx-glr-signature `Gallery generated by Sphinx-Gallery `_