mirror of
https://github.com/mfocko/blog.git
synced 2024-12-23 04:41:31 +01:00
30 lines
104 KiB
HTML
30 lines
104 KiB
HTML
|
<!doctype html>
|
|||
|
|
<html lang="en" dir="ltr" class="docs-wrapper docs-doc-page docs-version-current plugin-docs plugin-id-ib002 docs-doc-id-algorithms-correctness/postcondition-ambiguity">
|
|||
|
|
<head>
|
|||
|
|
<meta charset="UTF-8">
|
|||
|
|
<meta name="generator" content="Docusaurus v2.4.1">
|
|||
|
|
<title data-rh="true">Vague postconditions and proving correctness of algorithms | mf</title><meta data-rh="true" name="viewport" content="width=device-width,initial-scale=1"><meta data-rh="true" name="twitter:card" content="summary_large_image"><meta data-rh="true" property="og:url" content="https://blog.mfocko.xyz/ib002/algorithms-correctness/postcondition-ambiguity"><meta data-rh="true" name="docusaurus_locale" content="en"><meta data-rh="true" name="docsearch:language" content="en"><meta data-rh="true" name="docusaurus_version" content="current"><meta data-rh="true" name="docusaurus_tag" content="docs-ib002-current"><meta data-rh="true" name="docsearch:version" content="current"><meta data-rh="true" name="docsearch:docusaurus_tag" content="docs-ib002-current"><meta data-rh="true" property="og:title" content="Vague postconditions and proving correctness of algorithms | mf"><meta data-rh="true" name="description" content="Debugging and testing with precise postconditions.
|
|||
|
|
"><meta data-rh="true" property="og:description" content="Debugging and testing with precise postconditions.
|
|||
|
|
"><link data-rh="true" rel="icon" href="/img/favicon.ico"><link data-rh="true" rel="canonical" href="https://blog.mfocko.xyz/ib002/algorithms-correctness/postcondition-ambiguity"><link data-rh="true" rel="alternate" href="https://blog.mfocko.xyz/ib002/algorithms-correctness/postcondition-ambiguity" hreflang="en"><link data-rh="true" rel="alternate" href="https://blog.mfocko.xyz/ib002/algorithms-correctness/postcondition-ambiguity" hreflang="x-default"><link data-rh="true" rel="preconnect" href="https://0VXRFPR4QF-dsn.algolia.net" crossorigin="anonymous"><link rel="search" type="application/opensearchdescription+xml" title="mf" href="/opensearch.xml">
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
<link rel="alternate" type="application/rss+xml" href="/blog/rss.xml" title="mf RSS Feed">
|
|||
|
|
<link rel="alternate" type="application/atom+xml" href="/blog/atom.xml" title="mf Atom Feed">
|
|||
|
|
<link rel="alternate" type="application/json" href="/blog/feed.json" title="mf JSON Feed">
|
|||
|
|
|
|||
|
|
|
|||
|
|
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.13.24/dist/katex.min.css" integrity="sha384-odtC+0UGzzFL/6PNoE8rX/SPcQDXBJ+uRepguP4QkPCm2LBxH3FA3y+fKSiJ+AmM" crossorigin="anonymous"><link rel="stylesheet" href="/assets/css/styles.8480cb83.css">
|
|||
|
|
<link rel="preload" href="/assets/js/runtime~main.be793c46.js" as="script">
|
|||
|
|
<link rel="preload" href="/assets/js/main.9283b308.js" as="script">
|
|||
|
|
</head>
|
|||
|
|
<body class="navigation-with-keyboard">
|
|||
|
|
<script>!function(){function t(t){document.documentElement.setAttribute("data-theme",t)}var e=function(){var t=null;try{t=new URLSearchParams(window.location.search).get("docusaurus-theme")}catch(t){}return t}()||function(){var t=null;try{t=localStorage.getItem("theme")}catch(t){}return t}();t(null!==e?e:"light")}()</script><div id="__docusaurus">
|
|||
|
|
<div role="region" aria-label="Skip to main content"><a class="skipToContent_fXgn" href="#__docusaurus_skipToContent_fallback">Skip to main content</a></div><nav aria-label="Main" class="navbar navbar--fixed-top"><div class="navbar__inner"><div class="navbar__items"><button aria-label="Toggle navigation bar" aria-expanded="false" class="navbar__toggle clean-btn" type="button"><svg width="30" height="30" viewBox="0 0 30 30" aria-hidden="true"><path stroke="currentColor" stroke-linecap="round" stroke-miterlimit="10" stroke-width="2" d="M4 7h22M4 15h22M4 23h22"></path></svg></button><a class="navbar__brand" href="/"><b class="navbar__title text--truncate">mf</b></a><div class="navbar__item dropdown dropdown--hoverable"><a href="#" aria-haspopup="true" aria-expanded="false" role="button" class="navbar__link">Additional FI MU materials</a><ul class="dropdown__menu"><li><a aria-current="page" class="dropdown__link dropdown__link--active" href="/ib002/">IB002: Algorithms</a></li><li><a class="dropdown__link" href="/pb071/">PB071: C</a></li><li><a class="dropdown__link" href="/pb161/">PB161: C++</a></li></ul></div><a class="navbar__item navbar__link" href="/contributions">Contributions</a><a class="navbar__item navbar__link" href="/talks">Talks</a></div><div class="navbar__items navbar__items--right"><a class="navbar__item navbar__link" href="/blog">Blog</a><div class="toggle_vylO colorModeToggle_DEke"><button class="clean-btn toggleButton_gllP toggleButtonDisabled_aARS" type="button" disabled="" title="Switch between dark and light mode (currently light mode)" aria-label="Switch between dark and light mode (currently light mode)" aria-live="polite"><svg viewBox="0 0 24 24" width="24" height="24" class="lightToggleIcon_pyhR"><path fill="currentColor" d="M12,9c1.65,0,3,1.35,3,3s-1.35,3-3,3s-3-1.35-3-3S10.35,9,12,9 M12,7c-2.76,0-5,2.24-5,5s2.24,5,5,5s5-2.24,5-5 S14.76,7,12,7L12,7z M2,13l2,0c0.55,0,1-0.45,1-1s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S1.45,13,2,13z M20,13l2,0c0.55,0,1-0.45,1-1 s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S19.45,13,20,13z M11,2v2c0,0.55,0.45,1,1,1s1-0.45,1-1V2c0-0.55-0.45-1-1-1S11,1.45,11,2z M11,20v2c0,0.55,0.45,1,1,1s1-0.45,1-1v-2c0-0.55-0.45-1-1-1C11.45,19,11,19.45,11,20z M5.99,4.58c-0.39-0.39-1.03-0.39-1.41,0 c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0s0.39-1.03,0-1.41L5.99,4.58z M18.36,16.95 c-0.39-0.39-1.03-0.39-1.41,0c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0c0.39-0.39,0.39-1.03,0-1.41 L18.36,16.95z M19.42,5.99c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06c-0.39,0.39-0.39,1.03,0,1.41 s1.03,0.39,1.41,0L19.42,5.99z M7.05,18.36c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06 c-0.39,0.39-0.39,1.03,0,1.41s1.03,0.39,1.41,0L7.05,18.36z"></path></svg><svg viewBox="0 0 24 24" width="24" height="24" class="darkToggleIcon_wfgR"><path fill="currentColor" d="M9.37,5.51C9.19,6.15,9.1,6.82,9.1,7.5c0,4.08,3.32,7.4,7.4,7.4c0.68,0,1.35-0.09,1.99-0.27C17.45,17.19,14.93,19,12,19 c-3.86,0-7-3.14-7-7C5,9.07,6.81,6.55,9.37,5.51z M12,3c-4.97,0-9,4.03-9,9s4.03,9,9,9s9-4.03,9-9c0-0.46-0.04-0.92-0.1-1.36 c-0.98,1.37-2.58,2.26-4.4,2.26c-2.98,0-5.4-2.42-5.4-5.4c0-1.81,0.89-3.42,2.26-4.4C12.92,3.04,12.46,3,12,3L12,3z"></path></svg></button></div><div class="searchBox_ZlJk"><button type="button" class="DocSearch DocSearch-Button" aria-label="Search"><span class="DocSearch-Button-Container"><svg width="20" height="20" class="DocSearch-Search-Icon" viewBox="0 0 20 20"><path d="M14.386 14.386l4.0877 4.0877-4.0877-4.0877c-2.9418 2.9419-7.7115 2.9419-10.6533 0-2.9419-2.9418-2.9419-7.7115 0-10.6533 2.9418-2.9419 7.7115-2.9419 10.6533 0 2.9419 2.9418 2.9419 7.7115 0 10.6533z" stroke="currentColor" fill="none" fill-rule="evenodd" stroke-linecap="round" stroke-linejoin="round"></path></svg><span class="DocSearch-Button-Placeholder">Search</span></span><span class="DocSearch-Button-Keys"></span></button></div></div></div><div role="presentation" class="navbar-sidebar__backdrop"></div></nav><div id="__docusaurus_skipToContent_fallback" class="main-wrapper mainWrapper_
|
|||
|
|
This will ensure that even if the maximum in the original array was the first element, I will always satisfy that 2nd part of the loop invariant.</li></ol><div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-color:#000000;--prism-background-color:#ffffff"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:rgb(0, 0, 255)">def</span><span class="token plain"> </span><span class="token function" style="color:rgb(0, 0, 255)">broken_select_sort</span><span class="token punctuation" style="color:rgb(4, 81, 165)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:rgb(4, 81, 165)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:rgb(4, 81, 165)">)</span><span class="token punctuation" style="color:rgb(4, 81, 165)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(0, 0, 255)">assert</span><span class="token plain"> n </span><span class="token operator" style="color:rgb(0, 0, 0)">==</span><span class="token plain"> </span><span class="token builtin" style="color:rgb(0, 112, 193)">len</span><span class="token punctuation" style="color:rgb(4, 81, 165)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:rgb(4, 81, 165)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain" style="display:inline-block"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(0, 0, 255)">if</span><span class="token plain"> </span><span class="token keyword" style="color:rgb(0, 0, 255)">not</span><span class="token plain"> arr</span><span class="token punctuation" style="color:rgb(4, 81, 165)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:rgb(0, 0, 255)">return</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain" style="display:inline-block"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> max_value </span><span class="token operator" style="color:rgb(0, 0, 0)">=</span><span class="token plain"> </span><span class="token builtin" style="color:rgb(0, 112, 193)">max</span><span class="token punctuation" style="color:rgb(4, 81, 165)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:rgb(4, 81, 165)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain" style="display:inline-block"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:#000000"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> check_loop_invariant</span><span class="tok
|
|||
|
|
The reason why they are separated is pretty simple, this way they act like cartesian product: for each sorting function we also use each postcondition.</p></li><li><p><code>@settings</code> raises the count of tests that hypothesis runs (from default of 100(?)).</p></li><li><p><code>@given(lists(integers()))</code>
|
|||
|
|
This means hypothesis is randomly creating lists of integers and passing them to the function, which has only one parameter left and that is <code>numbers</code>.</p></li></ol><h3 class="anchor anchorWithStickyNavbar_LWe7" id="lets-run-the-tests">Let's run the tests!<a href="#lets-run-the-tests" class="hash-link" aria-label="Direct link to Let's run the tests!" title="Direct link to Let's run the tests!"></a></h3><p>In case you want to experiment locally, you should install <code>pytest</code> and <code>hypothesis</code> from the PyPI.</p><div class="codeBlockContainer_Ckt0 theme-code-block" style="--prism-color:#000000;--prism-background-color:#ffffff"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-text codeBlock_bY9V thin-scrollbar"><code class="codeBlockLines_e6Vv"><span class="token-line" style="color:#000000"><span class="token plain">% pytest -v test_sort.py</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">=================================== test session starts ====================================</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">platform linux -- Python 3.6.8, pytest-3.8.2, py-1.7.0, pluggy-0.13.1 -- /usr/bin/python3</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">cachedir: .pytest_cache</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">rootdir: /home/xfocko/git/xfocko/ib002/postcondition-ambiguity, inifile:</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">plugins: hypothesis-5.16.1</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">collected 4 items</span><br></span><span class="token-line" style="color:#000000"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#000000"><span class="token plain">test_sort.py::test_select_sort[select_sort-check_vague_postcondition] PASSED [ 25%]</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">test_sort.py::test_select_sort[select_sort-check_postcondition] PASSED [ 50%]</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">test_sort.py::test_select_sort[broken_select_sort-check_vague_postcondition] PASSED [ 75%]</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">test_sort.py::test_select_sort[broken_select_sort-check_postcondition] FAILED [100%]</span><br></span><span class="token-line" style="color:#000000"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#000000"><span class="token plain">========================================= FAILURES =========================================</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">_________________ test_select_sort[broken_select_sort-check_postcondition] _________________</span><br></span><span class="token-line" style="color:#000000"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#000000"><span class="token plain">sorting_function = <function broken_select_sort at 0x7fac179308c8></span><br></span><span class="token-line" style="color:#000000"><span class="token plain">postcondition = <function check_postcondition at 0x7fac1786d1e0></span><br></span><span class="token-line" style="color:#000000"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:#000000"><span class="token plain"> @given(lists(integers()))</span><br></span><span class="token-line" style="color:#000000"><span class="token plain">> @settings(max_examples=1000)</span><br></span><span class="token-line" style="color:#000000"><span class="token plain"> @pytest.mark.parametrize(</span><br></span><span class="token-li
|
|||
|
|
<script src="/assets/js/runtime~main.be793c46.js"></script>
|
|||
|
|
<script src="/assets/js/main.9283b308.js"></script>
|
|||
|
|
</body>
|
|||
|
|
</html>
|