<titledata-rh="true">Vague postconditions and proving correctness of algorithms | mf</title><metadata-rh="true"name="viewport"content="width=device-width,initial-scale=1"><metadata-rh="true"name="twitter:card"content="summary_large_image"><metadata-rh="true"property="og:url"content="https://blog.mfocko.xyz/ib002/algorithms-correctness/postcondition-ambiguity/"><metadata-rh="true"name="docusaurus_locale"content="en"><metadata-rh="true"name="docsearch:language"content="en"><metadata-rh="true"name="docusaurus_version"content="current"><metadata-rh="true"name="docusaurus_tag"content="docs-ib002-current"><metadata-rh="true"name="docsearch:version"content="current"><metadata-rh="true"name="docsearch:docusaurus_tag"content="docs-ib002-current"><metadata-rh="true"property="og:title"content="Vague postconditions and proving correctness of algorithms | mf"><metadata-rh="true"name="description"content="Debuggingandtestingwithprecisepostconditions.
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><divclass="language-py codeBlockContainer_Ckt0 theme-code-block"style="--prism-color:#000000;--prism-background-color:#ffffff"><divclass="codeBlockContent_biex"><pretabindex="0"class="prism-code language-py codeBlock_bY9V thin-scrollbar"><codeclass="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token keyword"style="color:rgb(0, 0, 255)">def</span><spanclass="token plain"></span><spanclass="token function"style="color:rgb(0, 0, 255)">broken_select_sort</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">(</span><spanclass="token plain">arr</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">,</span><spanclass="token plain"> n</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">)</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">:</span><spanclass="token plain"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"></span><spanclass="token keyword"style="color:rgb(0, 0, 255)">assert</span><spanclass="token plain"> n </span><spanclass="token operator"style="color:rgb(0, 0, 0)">==</span><spanclass="token plain"></span><spanclass="token builtin"style="color:rgb(0, 112, 193)">len</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">(</span><spanclass="token plain">arr</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">)</span><spanclass="token plain"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"style="display:inline-block"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"></span><spanclass="token keyword"style="color:rgb(0, 0, 255)">if</span><spanclass="token plain"></span><spanclass="token keyword"style="color:rgb(0, 0, 255)">not</span><spanclass="token plain"> arr</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">:</span><spanclass="token plain"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"></span><spanclass="token keyword"style="color:rgb(0, 0, 255)">return</span><spanclass="token plain"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"style="display:inline-block"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"> max_value </span><spanclass="token operator"style="color:rgb(0, 0, 0)">=</span><spanclass="token plain"></span><spanclass="token builtin"style="color:rgb(0, 112, 193)">max</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">(</span><spanclass="token plain">arr</span><spanclass="token punctuation"style="color:rgb(4, 81, 165)">)</span><spanclass="token plain"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"style="display:inline-block"></span></span><br></span><spanclass="token-line codeLine_lJS_"style="color:#000000"><spanclass="codeLineNumber_Tfdd"></span><spanclass="codeLineContent_feaV"><spanclass="token plain"> check_loop_invariant</span><spanclass="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><h3class="anchor anchorWithStickyNavbar_LWe7"id="lets-run-the-tests">Let's run the tests!<ahref="#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><divclass="codeBlockContainer_Ckt0 theme-code-block"style="--prism-color:#000000;--prism-background-color:#ffffff"><divclass="codeBlockContent_biex"><pretabindex="0"class="prism-code language-text codeBlock_bY9V thin-scrollbar"><codeclass="codeBlockLines_e6Vv"><spanclass="token-line"style="color:#000000"><spanclass="token plain">% pytest -v test_sort.py</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">=================================== test session starts ====================================</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="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><spanclass="token-line"style="color:#000000"><spanclass="token plain">cachedir: .pytest_cache</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">rootdir: /home/xfocko/git/xfocko/ib002/postcondition-ambiguity, inifile:</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">plugins: hypothesis-5.16.1</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">collected 4 items</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"style="display:inline-block"></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">test_sort.py::test_select_sort[select_sort-check_vague_postcondition] PASSED [ 25%]</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">test_sort.py::test_select_sort[select_sort-check_postcondition] PASSED [ 50%]</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">test_sort.py::test_select_sort[broken_select_sort-check_vague_postcondition] PASSED [ 75%]</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">test_sort.py::test_select_sort[broken_select_sort-check_postcondition] FAILED [100%]</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"style="display:inline-block"></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">========================================= FAILURES =========================================</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">_________________ test_select_sort[broken_select_sort-check_postcondition] _________________</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"style="display:inline-block"></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">sorting_function = <function broken_select_sort at 0x7fac179308c8></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">postcondition = <function check_postcondition at 0x7fac1786d1e0></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"style="display:inline-block"></span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"> @given(lists(integers()))</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain">> @settings(max_examples=1000)</span><br></span><spanclass="token-line"style="color:#000000"><spanclass="token plain"> @pytest.mark.parametrize(</span><br></span><spanclass="token-li
