mirror of
https://github.com/mfocko/blog.git
synced 2024-12-23 12:51:30 +01:00
128 lines
No EOL
109 KiB
HTML
128 lines
No EOL
109 KiB
HTML
<!doctype html>
|
||
<html lang="en" dir="ltr" class="docs-wrapper plugin-docs plugin-id-algorithms docs-version-current docs-doc-page docs-doc-id-algorithms-correctness/postcondition-ambiguity" data-has-hydrated="false">
|
||
<head>
|
||
<meta charset="UTF-8">
|
||
<meta name="generator" content="Docusaurus v3.0.0">
|
||
<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/algorithms/algorithms-correctness/postcondition-ambiguity/"><meta data-rh="true" property="og:locale" content="en"><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-algorithms-current"><meta data-rh="true" name="docsearch:version" content="current"><meta data-rh="true" name="docsearch:docusaurus_tag" content="docs-algorithms-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/algorithms/algorithms-correctness/postcondition-ambiguity/"><link data-rh="true" rel="alternate" href="https://blog.mfocko.xyz/algorithms/algorithms-correctness/postcondition-ambiguity/" hreflang="en"><link data-rh="true" rel="alternate" href="https://blog.mfocko.xyz/algorithms/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.b9f07789.css">
|
||
<script src="/assets/js/runtime~main.7784bcb4.js" defer="defer"></script>
|
||
<script src="/assets/js/main.93ba00d4.js" defer="defer"></script>
|
||
</head>
|
||
<body class="navigation-with-keyboard">
|
||
<script>!function(){function t(t){document.documentElement.setAttribute("data-theme",t)}var e=function(){try{return new URLSearchParams(window.location.search).get("docusaurus-theme")}catch(t){}}()||function(){try{return localStorage.getItem("theme")}catch(t){}}();t(null!==e?e:"light")}(),function(){try{const c=new URLSearchParams(window.location.search).entries();for(var[t,e]of c)if(t.startsWith("docusaurus-data-")){var a=t.replace("docusaurus-data-","data-");document.documentElement.setAttribute(a,e)}}catch(t){}}()</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="/algorithms/">Algorithms</a></li><li><a class="dropdown__link" href="/c/">C</a></li><li><a class="dropdown__link" href="/cpp/">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="navbarSearchContainer_Bca1"><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_z2l0"><div class="docsWrapper_hBAB"><button aria-label="Scroll back to top" class="clean-btn theme-back-to-top-button backToTopButton_sjWU" type="button"></button><div class="docRoot_UBD9"><aside class="theme-doc-sidebar-container docSidebarContainer_YfHR"><div class="sidebarViewport_aRkj"><div class="sidebar_njMd"><nav aria-label="Docs sidebar" class="menu thin-scrollbar menu_SIkG"><ul class="theme-doc-sidebar-menu menu__list"><li class="theme-doc-sidebar-item-link theme-doc-sidebar-item-link-level-1 menu__list-item"><a class="menu__link" href="/algorithms/">Introduction</a></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist menu__link--active" aria-expanded="true" href="/algorithms/category/algorithms-and-correctness/">Algorithms and Correctness</a><button aria-label="Collapse sidebar category 'Algorithms and Correctness'" type="button" class="clean-btn menu__caret"></button></div><ul style="display:block;overflow:visible;height:auto" class="menu__list"><li class="theme-doc-sidebar-item-link theme-doc-sidebar-item-link-level-2 menu__list-item"><a class="menu__link menu__link--active" aria-current="page" tabindex="0" href="/algorithms/algorithms-correctness/postcondition-ambiguity/">Vague postconditions and proving correctness of algorithms</a></li></ul></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/asymptotic-notation-and-time-complexity/">Asymptotic Notation and Time Complexity</a><button aria-label="Expand sidebar category 'Asymptotic Notation and Time Complexity'" type="button" class="clean-btn menu__caret"></button></div></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/recursion/">Recursion</a><button aria-label="Expand sidebar category 'Recursion'" type="button" class="clean-btn menu__caret"></button></div></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/red-black-trees/">Red-Black Trees</a><button aria-label="Expand sidebar category 'Red-Black Trees'" type="button" class="clean-btn menu__caret"></button></div></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/graphs/">Graphs</a><button aria-label="Expand sidebar category 'Graphs'" type="button" class="clean-btn menu__caret"></button></div></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/paths-in-graphs/">Paths in Graphs</a><button aria-label="Expand sidebar category 'Paths in Graphs'" type="button" class="clean-btn menu__caret"></button></div></li><li class="theme-doc-sidebar-item-category theme-doc-sidebar-item-category-level-1 menu__list-item menu__list-item--collapsed"><div class="menu__list-item-collapsible"><a class="menu__link menu__link--sublist" aria-expanded="false" href="/algorithms/category/hash-tables/">Hash Tables</a><button aria-label="Expand sidebar category 'Hash Tables'" type="button" class="clean-btn menu__caret"></button></div></li></ul></nav><button type="button" title="Collapse sidebar" aria-label="Collapse sidebar" class="button button--secondary button--outline collapseSidebarButton_PEFL"><svg width="20" height="20" aria-hidden="true" class="collapseSidebarButtonIcon_kv0_"><g fill="#7a7a7a"><path d="M9.992 10.023c0 .2-.062.399-.172.547l-4.996 7.492a.982.982 0 01-.828.454H1c-.55 0-1-.453-1-1 0-.2.059-.403.168-.551l4.629-6.942L.168 3.078A.939.939 0 010 2.528c0-.548.45-.997 1-.997h2.996c.352 0 .649.18.828.45L9.82 9.472c.11.148.172.347.172.55zm0 0"></path><path d="M19.98 10.023c0 .2-.058.399-.168.547l-4.996 7.492a.987.987 0 01-.828.454h-3c-.547 0-.996-.453-.996-1 0-.2.059-.403.168-.551l4.625-6.942-4.625-6.945a.939.939 0 01-.168-.55 1 1 0 01.996-.997h3c.348 0 .649.18.828.45l4.996 7.492c.11.148.168.347.168.55zm0 0"></path></g></svg></button></div></div></aside><main class="docMainContainer_TBSr"><div class="container padding-top--md padding-bottom--lg"><div class="row"><div class="col docItemCol_VOVn"><div class="docItemContainer_Djhp"><article><nav class="theme-doc-breadcrumbs breadcrumbsContainer_Z_bl" aria-label="Breadcrumbs"><ul class="breadcrumbs" itemscope="" itemtype="https://schema.org/BreadcrumbList"><li class="breadcrumbs__item"><a aria-label="Home page" class="breadcrumbs__link" href="/"><svg viewBox="0 0 24 24" class="breadcrumbHomeIcon_YNFT"><path d="M10 19v-5h4v5c0 .55.45 1 1 1h3c.55 0 1-.45 1-1v-7h1.7c.46 0 .68-.57.33-.87L12.67 3.6c-.38-.34-.96-.34-1.34 0l-8.36 7.53c-.34.3-.13.87.33.87H5v7c0 .55.45 1 1 1h3c.55 0 1-.45 1-1z" fill="currentColor"></path></svg></a></li><li itemscope="" itemprop="itemListElement" itemtype="https://schema.org/ListItem" class="breadcrumbs__item"><a class="breadcrumbs__link" itemprop="item" href="/algorithms/category/algorithms-and-correctness/"><span itemprop="name">Algorithms and Correctness</span></a><meta itemprop="position" content="1"></li><li itemscope="" itemprop="itemListElement" itemtype="https://schema.org/ListItem" class="breadcrumbs__item breadcrumbs__item--active"><span class="breadcrumbs__link" itemprop="name">Vague postconditions and proving correctness of algorithms</span><meta itemprop="position" content="2"></li></ul></nav><div class="tocCollapsible_ETCw theme-doc-toc-mobile tocMobile_ITEo"><button type="button" class="clean-btn tocCollapsibleButton_TO0P">On this page</button></div><div class="theme-doc-markdown markdown"><header><h1>Vague postconditions and proving correctness of algorithms</h1></header><h2 class="anchor anchorWithStickyNavbar_LWe7" id="introduction">Introduction<a href="#introduction" class="hash-link" aria-label="Direct link to Introduction" title="Direct link to Introduction"></a></h2>
|
||
<p><a href="/files/algorithms/algorithms-correctness/postcondition-ambiguity/test_sort.py" target="_blank" rel="noopener noreferrer">Source code</a> used later on.</p>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="implementation-of-select-sort-from-the-exercises">Implementation of select sort from the exercises<a href="#implementation-of-select-sort-from-the-exercises" class="hash-link" aria-label="Direct link to Implementation of select sort from the exercises" title="Direct link to Implementation of select sort from the exercises"></a></h2>
|
||
<p>To implement select sort from the exercises and make it as easy to read as possible, I have implemented maximum function that returns index of the biggest element from the first <span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4306em"></span><span class="mord mathnormal">n</span></span></span></span> elements.</p>
|
||
<p>For the sake of time and memory complexity, I am also using <code>itertools.islice</code>, which makes a slice, but does not copy the elements into the memory like normal slice does.</p>
|
||
<p>There is also a <code>check_loop_invariant</code> function that will be described later.</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">compare_by_value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">pair</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> index</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> value </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> pair</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"> value</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">maximum</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> first_n_elements </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token builtin" style="color:hsl(119, 34%, 47%)">enumerate</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> index</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> value </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">max</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">first_n_elements</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> key</span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain">compare_by_value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"> index</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> n </span><span class="token operator" style="color:hsl(221, 87%, 60%)">==</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> check_loop_invariant</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> i </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">reversed</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token builtin" style="color:hsl(119, 34%, 47%)">range</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> j </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> maximum</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">j</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">j</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> check_loop_invariant</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"> arr</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="discussed-preconditions-loop-invariants-and-postconditions">Discussed preconditions, loop invariants and postconditions<a href="#discussed-preconditions-loop-invariants-and-postconditions" class="hash-link" aria-label="Direct link to Discussed preconditions, loop invariants and postconditions" title="Direct link to Discussed preconditions, loop invariants and postconditions"></a></h2>
|
||
<p>You can safely replace <code>A</code> with <code>arr</code> or array for list.</p>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="precondition">Precondition<a href="#precondition" class="hash-link" aria-label="Direct link to Precondition" title="Direct link to Precondition"></a></h3>
|
||
<p>As a precondition we have established that <code>A</code> represents an array of values and <span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4306em"></span><span class="mord mathnormal">n</span></span></span></span> is length of the <code>A</code>.</p>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="loop-invariant">Loop invariant<a href="#loop-invariant" class="hash-link" aria-label="Direct link to Loop invariant" title="Direct link to Loop invariant"></a></h3>
|
||
<p>As for loop invariant we have established that we require two properties:</p>
|
||
<ol>
|
||
<li><code>A[i + 1 : n]</code> is sorted</li>
|
||
<li>all elements of <code>A[i + 1 : n]</code> are bigger or equal to the other elements</li>
|
||
</ol>
|
||
<p>This invariant is later defined as <code>check_loop_invariant</code> function. It is checked before the first iteration and after each iteration.</p>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="postcondition">Postcondition<a href="#postcondition" class="hash-link" aria-label="Direct link to Postcondition" title="Direct link to Postcondition"></a></h3>
|
||
<p>For the postcondition the first suggestion was that <code>A</code> must be sorted. And later we have added that <code>A'</code> must be a permutation of <code>A</code>.</p>
|
||
<blockquote>
|
||
<p>However at the end of the session question arose if it is really required to state in the postcondition that <code>A'</code> is a permutation.</p>
|
||
</blockquote>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="so-is-the-permutation-really-required">So is the permutation really required?<a href="#so-is-the-permutation-really-required" class="hash-link" aria-label="Direct link to So is the permutation really required?" title="Direct link to So is the permutation really required?"></a></h2>
|
||
<p>As I have said it is better to have postconditions explicit and do not expect anything that is not stated explicitly, e.g. <em>name suggests it</em>. In reality we could consider it as a smaller mistake (but it has consequences).</p>
|
||
<p>On the other hand explicit postconditions can be used to our advantage <strong>and also</strong> help our proof of correctness.</p>
|
||
<p>Consequences:</p>
|
||
<ol>
|
||
<li>
|
||
<p>Property-based testing</p>
|
||
<p>If we have explicit postconditions we can use them to define properties of the output from our algorithms. That way we can use property-based testing, which does not depend on specific inputs and expected outputs, but rather on randomly generated input and checking if the output conforms to our expectations (the postconditions are fulfilled).</p>
|
||
</li>
|
||
<li>
|
||
<p>Proof of correctness</p>
|
||
<p>If we can prove that algorithm is correct even for algorithm that <strong>is not</strong> correct, we have a problem. That proof has no value and is useless.</p>
|
||
</li>
|
||
</ol>
|
||
<p>For the sake of showcasing the power of postconditions I will introduce "select sort" that is not correct, but will comply with both the loop invariant and our vague postcondition and thus pass the tests.</p>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="implementation-of-the-broken-select-sort">Implementation of the broken select sort<a href="#implementation-of-the-broken-select-sort" class="hash-link" aria-label="Direct link to Implementation of the broken select sort" title="Direct link to Implementation of the broken select sort"></a></h2>
|
||
<p>To make sure this thing passes everything, but our explicit postcondition with permutation will <em>blow it up</em>, I have designed this "select sort" as follows:</p>
|
||
<ol>
|
||
<li>If I get empty list, there is nothing to do.</li>
|
||
<li>I find maximum in the array.</li>
|
||
<li>For each index from the end, I will assign <code>maximum + index</code>.
|
||
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-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">broken_select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> n </span><span class="token operator" style="color:hsl(221, 87%, 60%)">==</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">if</span><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">not</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> max_value </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">max</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> check_loop_invariant</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> i </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">reversed</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token builtin" style="color:hsl(119, 34%, 47%)">range</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> max_value </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> i</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> check_loop_invariant</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"> arr</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<div class="theme-admonition theme-admonition-tip admonition_xJq3 alert alert--success"><div class="admonitionHeading_Gvgb"><span class="admonitionIcon_Rf37"><svg viewBox="0 0 12 16"><path fill-rule="evenodd" d="M6.5 0C3.48 0 1 2.19 1 5c0 .92.55 2.25 1 3 1.34 2.25 1.78 2.78 2 4v1h5v-1c.22-1.22.66-1.75 2-4 .45-.75 1-2.08 1-3 0-2.81-2.48-5-5.5-5zm3.64 7.48c-.25.44-.47.8-.67 1.11-.86 1.41-1.25 2.06-1.45 3.23-.02.05-.02.11-.02.17H5c0-.06 0-.13-.02-.17-.2-1.17-.59-1.83-1.45-3.23-.2-.31-.42-.67-.67-1.11C2.44 6.78 2 5.65 2 5c0-2.2 2.02-4 4.5-4 1.22 0 2.36.42 3.22 1.19C10.55 2.94 11 3.94 11 5c0 .66-.44 1.78-.86 2.48zM4 14h5c-.23 1.14-1.3 2-2.5 2s-2.27-.86-2.5-2z"></path></svg></span>tip</div><div class="admonitionContent_BuS1"><p>There is also an easier way to break this, I leave that as an exercise ;)</p></div></div>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="property-based-tests-for-our-sorts">Property-based tests for our sorts<a href="#property-based-tests-for-our-sorts" class="hash-link" aria-label="Direct link to Property-based tests for our sorts" title="Direct link to Property-based tests for our sorts"></a></h2>
|
||
<p>Since we have talked a lot about proofs at the seminar, I would like to demonstrate it on the testing of the sorts. In the following text I will cover implementation of the loop invariant and both postconditions we have talked about and then test our sorts using them.</p>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="loop-invariant-1">Loop invariant<a href="#loop-invariant-1" class="hash-link" aria-label="Direct link to Loop invariant" title="Direct link to Loop invariant"></a></h3>
|
||
<p>To check loop invariant I have implemented this function:</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">check_loop_invariant</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># A[i + 1 : n] is sorted</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> x</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> y </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">zip</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">2</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> x </span><span class="token operator" style="color:hsl(221, 87%, 60%)"><=</span><span class="token plain"> y</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># all elements of A[i + 1 : n] are bigger or equal to the other elements</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">if</span><span class="token plain"> i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">>=</span><span class="token plain"> n</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># in case there are no elements</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># otherwise, since the "tail" is sorted, we can assume that it is enough to</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># check the other elements to the smallest value of the tail</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> smallest </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> element </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> i </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> smallest </span><span class="token operator" style="color:hsl(221, 87%, 60%)">>=</span><span class="token plain"> element</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>First part checks if the "ending" of the array is sorted.</p>
|
||
<p>In second part I have used a <em>dirty trick</em> of taking just the first element that is the smallest and compared the rest of the elements to it. Why is it enough? I leave it as an exercise ;)</p>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="postconditions">Postcondition(s)<a href="#postconditions" class="hash-link" aria-label="Direct link to Postcondition(s)" title="Direct link to Postcondition(s)"></a></h3>
|
||
<p>I have defined both the vague and explicit postconditions:</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">check_vague_postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">original_arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">if</span><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">not</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># check ordering</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> x</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> y </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">zip</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> x </span><span class="token operator" style="color:hsl(221, 87%, 60%)"><=</span><span class="token plain"> y</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">check_postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">original_arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">if</span><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">not</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">return</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># check ordering</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> x</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> y </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">zip</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> itertools</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">islice</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> x </span><span class="token operator" style="color:hsl(221, 87%, 60%)"><=</span><span class="token plain"> y</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># get counts from original list</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> original_counts </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">{</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">}</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> value </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> original_arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> original_counts</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> original_counts</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">get</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">0</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># get counts from resulting list</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> counts </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">{</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">}</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">for</span><span class="token plain"> value </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">in</span><span class="token plain"> arr</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> counts</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">1</span><span class="token plain"> </span><span class="token operator" style="color:hsl(221, 87%, 60%)">+</span><span class="token plain"> counts</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">get</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">value</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token number" style="color:hsl(35, 99%, 36%)">0</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token comment" style="color:hsl(230, 4%, 64%)"># if arr is permutation of original_arr then all counts must be the same</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">assert</span><span class="token plain"> counts </span><span class="token operator" style="color:hsl(221, 87%, 60%)">==</span><span class="token plain"> original_counts</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<h3 class="anchor anchorWithStickyNavbar_LWe7" id="putting-it-together">Putting it together<a href="#putting-it-together" class="hash-link" aria-label="Direct link to Putting it together" title="Direct link to Putting it together"></a></h3>
|
||
<p>Now that we have everything implement, we can move on to the implementation of the tests:</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">from</span><span class="token plain"> hypothesis </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">import</span><span class="token plain"> given</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> settings</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">from</span><span class="token plain"> hypothesis</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token plain">strategies </span><span class="token keyword" style="color:hsl(301, 63%, 40%)">import</span><span class="token plain"> integers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> lists</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">import</span><span class="token plain"> pytest</span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">@given</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">lists</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">integers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">@settings</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">max_examples</span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token number" style="color:hsl(35, 99%, 36%)">1000</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">@pytest</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">mark</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">parametrize</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> </span><span class="token string" style="color:hsl(119, 34%, 47%)">"postcondition"</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">check_vague_postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> check_postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">@pytest</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">mark</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">parametrize</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token string" style="color:hsl(119, 34%, 47%)">"sorting_function"</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> broken_select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"></span><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">test_select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">sorting_function</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> result </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> sorting_function</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain"> postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> result</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>Since it might seem a bit scary, I will disect it by parts.</p>
|
||
<ol>
|
||
<li>
|
||
<p>Parameters of test function</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token keyword" style="color:hsl(301, 63%, 40%)">def</span><span class="token plain"> </span><span class="token function" style="color:hsl(221, 87%, 60%)">test_select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">sorting_function</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>We are given 3 parameters:</p>
|
||
<ul>
|
||
<li><code>sorting_function</code> - as the name suggests is the sorting function we test</li>
|
||
<li><code>postcondition</code> - as the name suggests is the postcondition that we check</li>
|
||
<li><code>numbers</code> - is random list of numbers that we will be sorting</li>
|
||
</ul>
|
||
</li>
|
||
<li>
|
||
<p>Body of the test</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain">result </span><span class="token operator" style="color:hsl(221, 87%, 60%)">=</span><span class="token plain"> sorting_function</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">:</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token builtin" style="color:hsl(119, 34%, 47%)">len</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span><span class="token plain"></span></span><br></span><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token plain">postcondition</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token plain">numbers</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> result</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>We pass to the sorting function <strong>copy</strong> of the numbers we got, this ensures that once we are checking the more strict postcondition, we can gather the necessary information even after sorting the list in-situ, i.e. we can check if the <code>result</code> is really a <code>permutation</code> of the <code>numbers</code> even though the sorting functions has modified the passed in list.</p>
|
||
</li>
|
||
</ol>
|
||
<div class="theme-admonition theme-admonition-warning admonition_xJq3 alert alert--warning"><div class="admonitionHeading_Gvgb"><span class="admonitionIcon_Rf37"><svg viewBox="0 0 16 16"><path fill-rule="evenodd" d="M8.893 1.5c-.183-.31-.52-.5-.887-.5s-.703.19-.886.5L.138 13.499a.98.98 0 0 0 0 1.001c.193.31.53.501.886.501h13.964c.367 0 .704-.19.877-.5a1.03 1.03 0 0 0 .01-1.002L8.893 1.5zm.133 11.497H6.987v-2.003h2.039v2.003zm0-3.004H6.987V5.987h2.039v4.006z"></path></svg></span>caution</div><div class="admonitionContent_BuS1"><p>Now we get to the more complicated part and it is the <em>decorators</em>.</p></div></div>
|
||
<ol start="3">
|
||
<li>
|
||
<p>1st <code>parametrize</code> from the bottom</p>
|
||
<div class="language-py codeBlockContainer_Ckt0 theme-code-block" style="--prism-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-py codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv codeBlockLinesWithNumbering_o6Pm"><span class="token-line codeLine_lJS_" style="color:hsl(230, 8%, 24%)"><span class="codeLineNumber_Tfdd"></span><span class="codeLineContent_feaV"><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">@pytest</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">mark</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">.</span><span class="token decorator annotation punctuation" style="color:hsl(119, 34%, 47%)">parametrize</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">(</span><span class="token string" style="color:hsl(119, 34%, 47%)">"sorting_function"</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> </span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">[</span><span class="token plain">select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">,</span><span class="token plain"> broken_select_sort</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">]</span><span class="token punctuation" style="color:hsl(119, 34%, 47%)">)</span></span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>This tells pytest, that we want to pass the values from the list to the parameter <code>sorting_function</code>. In other words, this lets us use the same test function for both the correct and incorrect select sort.</p>
|
||
</li>
|
||
<li>
|
||
<p>2nd <code>parametrize</code> from the bottom is similar, but works with the postcondition.
|
||
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-background-color:hsl(230, 1%, 98%);--prism-color:hsl(230, 8%, 24%)"><div class="codeBlockContent_biex"><pre tabindex="0" class="prism-code language-text codeBlock_bY9V thin-scrollbar" style="background-color:hsl(230, 1%, 98%);color:hsl(230, 8%, 24%)"><code class="codeBlockLines_e6Vv"><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">% pytest -v test_sort.py</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">=================================== test session starts ====================================</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="token plain">cachedir: .pytest_cache</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">rootdir: /home/xfocko/git/xfocko/ib002/postcondition-ambiguity, inifile:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">plugins: hypothesis-5.16.1</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">collected 4 items</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><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:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">========================================= FAILURES =========================================</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">_________________ test_select_sort[broken_select_sort-check_postcondition] _________________</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">sorting_function = <function broken_select_sort at 0x7fac179308c8></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">postcondition = <function check_postcondition at 0x7fac1786d1e0></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> @given(lists(integers()))</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">> @settings(max_examples=1000)</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> @pytest.mark.parametrize(</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> "postcondition", [check_vague_postcondition, check_postcondition]</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> )</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> @pytest.mark.parametrize("sorting_function", [select_sort, broken_select_sort])</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> def test_select_sort(sorting_function, postcondition, numbers):</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">test_sort.py:132:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">test_sort.py:139: in test_select_sort</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> postcondition(numbers, result)</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">original_arr = [0, 0], arr = [0, 1]</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> def check_postcondition(original_arr, arr):</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> if not arr:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> return</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> # check ordering</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> for x, y in zip(arr, itertools.islice(arr, 1, len(arr))):</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> assert x <= y</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> # get counts from original list</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> original_counts = {}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> for value in original_arr:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> original_counts[value] = 1 + original_counts.get(value, 0)</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> # get counts from resulting list</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> counts = {}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> for value in arr:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> counts[value] = 1 + counts.get(value, 0)</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> # if arr is permutation of original_arr then all counts must be the same</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">> assert counts == original_counts</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E assert {0: 1, 1: 1} == {0: 2}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E Differing items:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E {0: 1} != {0: 2}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E Left contains more items:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E {1: 1}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E Full diff:</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E - {0: 1, 1: 1}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">E + {0: 2}</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain" style="display:inline-block"></span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">test_sort.py:128: AssertionError</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">----------------------------------- Captured stdout call -----------------------------------</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">Falsifying example: test_select_sort(</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> sorting_function=<function test_sort.broken_select_sort>,</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> postcondition=<function test_sort.check_postcondition>,</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain"> numbers=[0, 0],</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">)</span><br></span><span class="token-line" style="color:hsl(230, 8%, 24%)"><span class="token plain">============================ 1 failed, 3 passed in 6.84 seconds ============================</span><br></span></code></pre><div class="buttonGroup__atx"><button type="button" aria-label="Copy code to clipboard" title="Copy" class="clean-btn"><span class="copyButtonIcons_eSgA" aria-hidden="true"><svg viewBox="0 0 24 24" class="copyButtonIcon_y97N"><path fill="currentColor" d="M19,21H8V7H19M19,5H8A2,2 0 0,0 6,7V21A2,2 0 0,0 8,23H19A2,2 0 0,0 21,21V7A2,2 0 0,0 19,5M16,1H4A2,2 0 0,0 2,3V17H4V3H16V1Z"></path></svg><svg viewBox="0 0 24 24" class="copyButtonSuccessIcon_LjdS"><path fill="currentColor" d="M21,7L9,19L3.5,13.5L4.91,12.09L9,16.17L19.59,5.59L21,7Z"></path></svg></span></button></div></div></div>
|
||
<p>We can clearly see that our broken select sort has passed the <em>vague postcondition</em>, but the explicit one was not satisfied.</p>
|
||
<h2 class="anchor anchorWithStickyNavbar_LWe7" id="summary">Summary<a href="#summary" class="hash-link" aria-label="Direct link to Summary" title="Direct link to Summary"></a></h2>
|
||
<p>For proving the correctness of the algorithm it is better to be explicit than prove that algorithm is correct even though it is not. Being explicit also allows you to test smaller <em>chunks</em> of code better.</p></div><footer class="theme-doc-footer docusaurus-mt-lg"><div class="theme-doc-footer-tags-row row margin-bottom--sm"><div class="col"><b>Tags:</b><ul class="tags_jXut padding--none margin-left--sm"><li class="tag_QGVx"><a class="tag_zVej tagRegular_sFm0" href="/algorithms/tags/python/">python</a></li><li class="tag_QGVx"><a class="tag_zVej tagRegular_sFm0" href="/algorithms/tags/testing/">testing</a></li><li class="tag_QGVx"><a class="tag_zVej tagRegular_sFm0" href="/algorithms/tags/postconditions/">postconditions</a></li><li class="tag_QGVx"><a class="tag_zVej tagRegular_sFm0" href="/algorithms/tags/sorting/">sorting</a></li></ul></div></div><div class="theme-doc-footer-edit-meta-row row"><div class="col"><a href="https://github.com/mfocko/blog/tree/main/algorithms/02-algorithms-correctness/2021-03-18-postcondition-ambiguity.md" target="_blank" rel="noopener noreferrer" class="theme-edit-this-page"><svg fill="currentColor" height="20" width="20" viewBox="0 0 40 40" class="iconEdit_Z9Sw" aria-hidden="true"><g><path d="m34.5 11.7l-3 3.1-6.3-6.3 3.1-3q0.5-0.5 1.2-0.5t1.1 0.5l3.9 3.9q0.5 0.4 0.5 1.1t-0.5 1.2z m-29.5 17.1l18.4-18.5 6.3 6.3-18.4 18.4h-6.3v-6.2z"></path></g></svg>Edit this page</a></div><div class="col lastUpdated_vwxv"><span class="theme-last-updated">Last updated<!-- --> on <b><time datetime="2021-03-18T00:00:00.000Z">Mar 18, 2021</time></b></span></div></div></footer></article><nav class="pagination-nav docusaurus-mt-lg" aria-label="Docs pages"><a class="pagination-nav__link pagination-nav__link--prev" href="/algorithms/category/algorithms-and-correctness/"><div class="pagination-nav__sublabel">Previous</div><div class="pagination-nav__label">Algorithms and Correctness</div></a><a class="pagination-nav__link pagination-nav__link--next" href="/algorithms/category/asymptotic-notation-and-time-complexity/"><div class="pagination-nav__sublabel">Next</div><div class="pagination-nav__label">Asymptotic Notation and Time Complexity</div></a></nav></div></div><div class="col col--3"><div class="tableOfContents_bqdL thin-scrollbar theme-doc-toc-desktop"><ul class="table-of-contents table-of-contents__left-border"><li><a href="#introduction" class="table-of-contents__link toc-highlight">Introduction</a></li><li><a href="#implementation-of-select-sort-from-the-exercises" class="table-of-contents__link toc-highlight">Implementation of select sort from the exercises</a></li><li><a href="#discussed-preconditions-loop-invariants-and-postconditions" class="table-of-contents__link toc-highlight">Discussed preconditions, loop invariants and postconditions</a><ul><li><a href="#precondition" class="table-of-contents__link toc-highlight">Precondition</a></li><li><a href="#loop-invariant" class="table-of-contents__link toc-highlight">Loop invariant</a></li><li><a href="#postcondition" class="table-of-contents__link toc-highlight">Postcondition</a></li></ul></li><li><a href="#so-is-the-permutation-really-required" class="table-of-contents__link toc-highlight">So is the permutation really required?</a></li><li><a href="#implementation-of-the-broken-select-sort" class="table-of-contents__link toc-highlight">Implementation of the broken select sort</a></li><li><a href="#property-based-tests-for-our-sorts" class="table-of-contents__link toc-highlight">Property-based tests for our sorts</a><ul><li><a href="#loop-invariant-1" class="table-of-contents__link toc-highlight">Loop invariant</a></li><li><a href="#postconditions" class="table-of-contents__link toc-highlight">Postcondition(s)</a></li><li><a href="#putting-it-together" class="table-of-contents__link toc-highlight">Putting it together</a></li><li><a href="#lets-run-the-tests" class="table-of-contents__link toc-highlight">Let's run the tests!</a></li></ul></li><li><a href="#summary" class="table-of-contents__link toc-highlight">Summary</a></li></ul></div></div></div></div></main></div></div></div><footer class="footer footer--dark"><div class="container container-fluid"><div class="row footer__links"><div class="col footer__col"><div class="footer__title">Git</div><ul class="footer__items clean-list"><li class="footer__item"><a href="https://github.com/mfocko" target="_blank" rel="noopener noreferrer" class="footer__link-item">GitHub<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://gitlab.com/mfocko" target="_blank" rel="noopener noreferrer" class="footer__link-item">GitLab<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://git.mfocko.xyz/mfocko" target="_blank" rel="noopener noreferrer" class="footer__link-item">Gitea (self-hosted)<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li></ul></div><div class="col footer__col"><div class="footer__title">Social #1</div><ul class="footer__items clean-list"><li class="footer__item"><a href="https://www.linkedin.com/in/mfocko/" target="_blank" rel="noopener noreferrer" class="footer__link-item">LinkedIn<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://fosstodon.org/@m4tt_314" target="_blank" rel="noopener noreferrer" class="footer__link-item">Fosstodon<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://hachyderm.io/@m4tt_314" target="_blank" rel="noopener noreferrer" class="footer__link-item">Hachyderm.io<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li></ul></div><div class="col footer__col"><div class="footer__title">Social #2</div><ul class="footer__items clean-list"><li class="footer__item"><a href="https://twitter.com/m4tt_314" target="_blank" rel="noopener noreferrer" class="footer__link-item">Twitter<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://twitch.tv/m4tt_314" target="_blank" rel="noopener noreferrer" class="footer__link-item">Twitch<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li><li class="footer__item"><a href="https://ko-fi.com/m4tt_314" target="_blank" rel="noopener noreferrer" class="footer__link-item">Ko-fi<svg width="13.5" height="13.5" aria-hidden="true" viewBox="0 0 24 24" class="iconExternalLink_nPIU"><path fill="currentColor" d="M21 13v10h-21v-19h12v2h-10v15h17v-8h2zm3-12h-10.988l4.035 4-6.977 7.07 2.828 2.828 6.977-7.07 4.125 4.172v-11z"></path></svg></a></li></ul></div></div><div class="footer__bottom text--center"><div class="footer__copyright">Copyright © 2024 Matej Focko.</div></div></div></footer></div>
|
||
</body>
|
||
</html> |