levovix
/
Nim
огледало од https://github.com/nim-lang/Nim


			
				
					
						
						
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186
							<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!--  This file is generated by Nim. -->
<html xmlns="https://www.w3.org/1999/xhtml" xml:lang="en" lang="en" data-theme="auto">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>DrNim User Guide</title>

<!-- Google fonts -->
<link href='https://fonts.googleapis.com/css?family=Lato:400,600,900' rel='stylesheet' type='text/css'/>
<link href='https://fonts.googleapis.com/css?family=Source+Code+Pro:400,500,600' rel='stylesheet' type='text/css'/>

<!-- Favicon -->
<link rel="shortcut icon" href="data:image/x-icon;base64,AAABAAEAEBAAAAEAIABoBAAAFgAAACgAAAAQAAAAIAAAAAEAIAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AAAAAAUAAAAF////AP///wD///8A////AP///wD///8A////AP///wD///8A////AAAAAAIAAABbAAAAlQAAAKIAAACbAAAAmwAAAKIAAACVAAAAWwAAAAL///8A////AP///wD///8A////AAAAABQAAADAAAAAYwAAAA3///8A////AP///wD///8AAAAADQAAAGMAAADAAAAAFP///wD///8A////AP///wAAAACdAAAAOv///wD///8A////AP///wD///8A////AP///wD///8AAAAAOgAAAJ3///8A////AP///wAAAAAnAAAAcP///wAAAAAoAAAASv///wD///8A////AP///wAAAABKAAAAKP///wAAAABwAAAAJ////wD///8AAAAAgQAAABwAAACIAAAAkAAAAJMAAACtAAAAFQAAABUAAACtAAAAkwAAAJAAAACIAAAAHAAAAIH///8A////AAAAAKQAAACrAAAAaP///wD///8AAAAARQAAANIAAADSAAAARf///wD///8AAAAAaAAAAKsAAACk////AAAAADMAAACcAAAAnQAAABj///8A////AP///wAAAAAYAAAAGP///wD///8A////AAAAABgAAACdAAAAnAAAADMAAAB1AAAAwwAAAP8AAADpAAAAsQAAAE4AAAAb////AP///wAAAAAbAAAATgAAALEAAADpAAAA/wAAAMMAAAB1AAAAtwAAAOkAAAD/AAAA/wAAAP8AAADvAAAA3gAAAN4AAADeAAAA3gAAAO8AAAD/AAAA/wAAAP8AAADpAAAAtwAAAGUAAAA/AAAA3wAAAP8AAAD/AAAA/wAAAP8AAAD/AAAA/wAAAP8AAAD/AAAA/wAAAP8AAADfAAAAPwAAAGX///8A////AAAAAEgAAADtAAAAvwAAAL0AAADGAAAA7wAAAO8AAADGAAAAvQAAAL8AAADtAAAASP///wD///8A////AP///wD///8AAAAAO////wD///8A////AAAAAIcAAACH////AP///wD///8AAAAAO////wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A////AP///wD///8A//8AAP//AAD4HwAA7/cAAN/7AAD//wAAoYUAAJ55AACf+QAAh+EAAAAAAADAAwAA4AcAAP5/AAD//wAA//8AAA=="/>
<link rel="icon" type="image/png" sizes="32x32" href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAACAAAAAgCAYAAABzenr0AAAABmJLR0QA/wD/AP+gvaeTAAAACXBIWXMAAA3XAAAN1wFCKJt4AAAAB3RJTUUH4QQQEwksSS9ZWwAAAk1JREFUWMPtll2ITVEUx39nn/O7Y5qR8f05wtCUUr6ZIS++8pEnkZInPImneaCQ5METNdOkeFBKUhMPRIkHKfEuUZSUlGlKPN2TrgfncpvmnntnmlEyq1Z7t89/rf9a6+y99oZxGZf/XeIq61EdtgKXgdXA0xrYAvBjOIF1AI9zvjcC74BSpndrJPkBWDScTF8Aa4E3wDlgHbASaANmVqlcCnwHvgDvgVfAJ+AikAAvgfVZwLnSVZHZaOuKoQi3ZOMi4NkYkpe1p4J7A8BpYAD49hfIy/oqG0+hLomiKP2L5L+1ubn5115S+3OAn4EnwBlgMzCjyt6ZAnQCJ4A7wOs88iRJHvw50HoujuPBoCKwHWiosy8MdfZnAdcHk8dxXFJ3VQbQlCTJvRBCGdRbD4M6uc5glpY3eAihpN5S5w12diSEcCCEcKUO4ljdr15T76ur1FDDLIQQ3qv71EdDOe3Kxj3leRXyk+pxdWnFWod6Wt2bY3de3aSuUHcPBVimHs7mK9WrmeOF6lR1o9qnzskh2ar2qm1qizpfXaPeVGdlmGN5pb09qMxz1Xb1kLqgzn1RyH7JUXW52lr5e/Kqi9qpto7V1atuUzfnARrV7jEib1T76gG2qxdGmXyiekkt1GswPTtek0aBfJp6YySGBfWg2tPQ0FAYgf1stUfdmdcjarbYJEniKIq6gY/Aw+zWHAC+p2labGpqiorFYgGYCEzN7oQdQClN07O1/EfDyGgC0ALMBdYAi4FyK+4H3gLPsxfR1zRNi+NP7nH5J+QntnXe5B5mpfQAAAAASUVORK5CYII=">

<!-- CSS -->
<link rel="stylesheet" type="text/css" href="nimdoc.out.css?v=2.3.1">

<!-- JS -->
<script type="text/javascript" src="dochack.js?v=2.3.1"></script>
</head>
<body>
  <div class="document" id="documentId">
    <div class="container">
      <h1 class="title">DrNim User Guide</h1>
      <div class="row">
  <div class="three columns">
    <div class="theme-select-wrapper">
      <label for="theme-select">Theme:&nbsp;</label>
      <select id="theme-select" onchange="setTheme(this.value)">
        <option value="auto">🌗 Match OS</option>
        <option value="dark">🌑 Dark</option>
        <option value="light">🌕 Light</option>
      </select>
    </div>
    <div id="global-links">
      <ul class="simple-boot">
        <li><a href="manual.html">Manual</a></li>
        <li><a href="lib.html">Standard library</a></li>
        <li> <a id="indexLink" href="theindex.html">Index</a></li>
        <li><a href="compiler/theindex.html">Compiler docs</a></li>
        <li><a href="https://nim-lang.github.io/fusion/theindex.html">Fusion docs</a></li>
        <li><a href="https://nim-lang.github.io/Nim/">devel</a>, <a href="https://nim-lang.org/documentation.html">stable</a></li>
      </ul>
    </div>
    <div id="searchInputDiv">
      Search: <input type="search" id="searchInput"
        oninput="search()" />
    </div>
    <div class="search-groupby">
  Group by:
  <select onchange="groupBy(this.value)">
    <option value="section">Section</option>
    <option value="type">Type</option>
  </select>
</div>

    <ul class="simple simple-toc" id="toc-list">
  <li><a class="reference" id="introduction_toc" href="#introduction">Introduction</a></li>
<li><a class="reference" id="installation_toc" href="#installation">Installation</a></li>
<li><a class="reference" id="motivating-example_toc" href="#motivating-example">Motivating Example</a></li>
<li><a class="reference" id="preminus-postconditions-and-invariants_toc" href="#preminus-postconditions-and-invariants">Pre-, postconditions and invariants</a></li>
<ul class="simple"><li><a class="reference" id="preminus-postconditions-and-invariants-invariant_toc" href="#preminus-postconditions-and-invariants-invariant">Invariant</a></li>
<li><a class="reference" id="preminus-postconditions-and-invariants-requires_toc" href="#preminus-postconditions-and-invariants-requires">Requires</a></li>
<li><a class="reference" id="preminus-postconditions-and-invariants-ensures_toc" href="#preminus-postconditions-and-invariants-ensures">Ensures</a></li>
<li><a class="reference" id="preminus-postconditions-and-invariants-assume_toc" href="#preminus-postconditions-and-invariants-assume">Assume</a></li>
</ul><li><a class="reference" id="examplecolon-insertionsort_toc" href="#examplecolon-insertionsort">Example: insertionSort</a></li>
<li><a class="reference" id="syntax-of-propositions_toc" href="#syntax-of-propositions">Syntax of propositions</a></li>

</ul>

  </div>
  <div class="nine columns" id="content">
    <a href="https://github.com/nim-lang/Nim/tree/devel/doc/drnim.md#L1" class="link-seesrc" target="_blank">Source</a>&nbsp;&nbsp;
<a href="https://github.com/nim-lang/Nim/edit/devel/doc/drnim.md#L1" class="link-seesrc" target="_blank" >Edit</a>&nbsp;&nbsp;

    <div id="tocRoot"></div>
    
    <p class="module-desc"><table class="docinfo" frame="void" rules="none"><col class="docinfo-name" /><col class="docinfo-content" /><tbody valign="top"><tr><th class="docinfo-name">Author:</th><td>Andreas Rumpf</td></tr>
<tr><th class="docinfo-name">Version:</th><td>2.3.1</td></tr>
</tbody></table>
<h1><a class="toc-backref" id="introduction" href="#introduction">Introduction</a></h1><p>This document describes the usage of the <em>DrNim</em> tool. DrNim combines the Nim frontend with the <a class="reference external" href="https://github.com/Z3Prover/z3">Z3</a> proof engine, in order to allow verify/validate software written in Nim. DrNim's command-line options are the same as the Nim compiler's.</p>
<p>DrNim currently only checks the sections of your code that are marked via <tt class="docutils literal"><span class="pre"><span class="Identifier">staticBoundChecks</span><span class="Punctuation">:</span> <span class="Identifier">on</span></span></tt>:</p>
<p><pre class="listing"><span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">push</span> <span class="Identifier">staticBoundChecks</span><span class="Punctuation">:</span> <span class="Identifier">on</span><span class="Operator">.</span><span class="Punctuation">}</span>
<span class="Comment"># &lt;--- code section here ----&gt;</span>
<span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">pop</span><span class="Operator">.</span><span class="Punctuation">}</span></pre></p>
<p>DrNim currently only tries to prove array indexing or subrange checks, overflow errors are <em>not</em> prevented. Overflows will be checked for in the future.</p>
<p>Later versions of the <strong>Nim compiler</strong> will <strong>assume</strong> that the checks inside the <tt class="docutils literal"><span class="pre"><span class="Identifier">staticBoundChecks</span><span class="Punctuation">:</span> <span class="Identifier">on</span></span></tt> environment have been proven correct and so it will <strong>omit</strong> the runtime checks. If you do not want this behavior, use instead <tt class="docutils literal"><span class="pre"><span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">push</span> <span class="Identifier">staticBoundChecks</span><span class="Punctuation">:</span> <span class="Identifier">defined</span><span class="Punctuation">(</span><span class="Identifier">nimDrNim</span><span class="Punctuation">)</span><span class="Operator">.</span><span class="Punctuation">}</span></span></tt>. This way the Nim compiler remains unaware of the performed proofs but DrNim will prove your code.</p>

<h1><a class="toc-backref" id="installation" href="#installation">Installation</a></h1><p>Run <tt class="docutils literal"><span class="pre"><span class="program">koch</span> <span class="option">drnim</span></span></tt>, the executable will afterwards be in <tt class="docutils literal"><span class="pre">$nim/bin/drnim</span></tt>.</p>

<h1><a class="toc-backref" id="motivating-example" href="#motivating-example">Motivating Example</a></h1><p>The follow example highlights what DrNim can easily do, even without additional annotations:</p>
<p><pre class="listing"><span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">push</span> <span class="Identifier">staticBoundChecks</span><span class="Punctuation">:</span> <span class="Identifier">on</span><span class="Operator">.</span><span class="Punctuation">}</span>

<span class="Keyword">proc</span> <span class="Identifier">sum</span><span class="Punctuation">(</span><span class="Identifier">a</span><span class="Punctuation">:</span> <span class="Identifier">openArray</span><span class="Punctuation">[</span><span class="Identifier">int</span><span class="Punctuation">]</span><span class="Punctuation">)</span><span class="Punctuation">:</span> <span class="Identifier">int</span> <span class="Operator">=</span>
  <span class="Keyword">for</span> <span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">0.</span><span class="Operator">.</span><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Punctuation">:</span>
    <span class="Identifier">result</span> <span class="Operator">+=</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span>

<span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">pop</span><span class="Operator">.</span><span class="Punctuation">}</span>

<span class="Identifier">echo</span> <span class="Identifier">sum</span><span class="Punctuation">(</span><span class="Punctuation">[</span><span class="DecNumber">1</span><span class="Punctuation">,</span> <span class="DecNumber">2</span><span class="Punctuation">,</span> <span class="DecNumber">3</span><span class="Punctuation">]</span><span class="Punctuation">)</span></pre></p>
<p>This program contains a famous &quot;index out of bounds&quot; bug. DrNim detects it and produces the following error message:</p>
<pre>cannot prove: i &lt;= len(a) + -1; counter example: i -&gt; 0 a.len -&gt; 0 [IndexCheck]</pre>
<p>In other words for <tt class="docutils literal"><span class="pre"><span class="Identifier">i</span> <span class="Operator">==</span> <span class="DecNumber">0</span></span></tt> and <tt class="docutils literal"><span class="pre"><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span> <span class="Operator">==</span> <span class="DecNumber">0</span></span></tt> (for example!) there would be an index out of bounds error.</p>

<h1><a class="toc-backref" id="preminus-postconditions-and-invariants" href="#preminus-postconditions-and-invariants">Pre-, postconditions and invariants</a></h1><p>DrNim adds 4 additional annotations (pragmas) to Nim:</p>
<ul class="simple"><li><span id="requires_1">requires</span></li>
<li><span id="ensures_1">ensures</span></li>
<li><span id="invariant_1">invariant</span></li>
<li><span id="assume_1">assume</span></li>
</ul>
<p>These pragmas are ignored by the Nim compiler so that they don't have to be disabled via <tt class="docutils literal"><span class="pre"><span class="Keyword">when</span> <span class="Identifier">defined</span><span class="Punctuation">(</span><span class="Identifier">nimDrNim</span><span class="Punctuation">)</span></span></tt>.</p>

<h2><a class="toc-backref" id="preminus-postconditions-and-invariants-invariant" href="#preminus-postconditions-and-invariants-invariant">Invariant</a></h2><p>An <tt class="docutils literal"><span class="pre"><span class="Identifier">invariant</span></span></tt> is a proposition that must be true after every loop iteration, it's tied to the loop body it's part of.</p>

<h2><a class="toc-backref" id="preminus-postconditions-and-invariants-requires" href="#preminus-postconditions-and-invariants-requires">Requires</a></h2><p>A <tt class="docutils literal"><span class="pre"><span class="Identifier">requires</span></span></tt> annotation describes what the function expects to be true before it's called so that it can perform its operation. A <tt class="docutils literal"><span class="pre"><span class="Identifier">requires</span></span></tt> annotation is also called a <span id="precondition_1">precondition</span>.</p>

<h2><a class="toc-backref" id="preminus-postconditions-and-invariants-ensures" href="#preminus-postconditions-and-invariants-ensures">Ensures</a></h2><p>An <tt class="docutils literal"><span class="pre"><span class="Identifier">ensures</span></span></tt> annotation describes what will be true after the function call. An <tt class="docutils literal"><span class="pre"><span class="Identifier">ensures</span></span></tt> annotation is also called a <span id="postcondition_1">postcondition</span>.</p>

<h2><a class="toc-backref" id="preminus-postconditions-and-invariants-assume" href="#preminus-postconditions-and-invariants-assume">Assume</a></h2><p>An <tt class="docutils literal"><span class="pre"><span class="Identifier">assume</span></span></tt> annotation describes what DrNim should <strong>assume</strong> to be true in this section of the program. It is an unsafe escape mechanism comparable to Nim's <tt class="docutils literal"><span class="pre"><span class="Keyword">cast</span></span></tt> statement. Use it only when you really know better than DrNim. You should add a comment to a paper that proves the proposition you assume.</p>

<h1><a class="toc-backref" id="examplecolon-insertionsort" href="#examplecolon-insertionsort">Example: insertionSort</a></h1><p><strong>Note</strong>: This example does not yet work with DrNim.</p>
<p><pre class="listing"><span class="Keyword">import</span> <span class="Identifier">std</span> <span class="Operator">/</span> <span class="Identifier">logic</span>

<span class="Keyword">proc</span> <span class="Identifier">insertionSort</span><span class="Punctuation">(</span><span class="Identifier">a</span><span class="Punctuation">:</span> <span class="Keyword">var</span> <span class="Identifier">openArray</span><span class="Punctuation">[</span><span class="Identifier">int</span><span class="Punctuation">]</span><span class="Punctuation">)</span> <span class="Punctuation">{</span><span class="Operator">.</span>
    <span class="Identifier">ensures</span><span class="Punctuation">:</span> <span class="Identifier">forall</span><span class="Punctuation">(</span><span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">1.</span><span class="Operator">.&lt;</span><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Punctuation">,</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Operator">-</span><span class="DecNumber">1</span><span class="Punctuation">]</span> <span class="Operator">&lt;=</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span><span class="Punctuation">)</span><span class="Operator">.</span><span class="Punctuation">}</span> <span class="Operator">=</span>
  
  <span class="Keyword">for</span> <span class="Identifier">k</span> <span class="Keyword">in</span> <span class="DecNumber">1</span> <span class="Operator">..&lt;</span> <span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Punctuation">:</span>
    <span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="DecNumber">1</span> <span class="Operator">&lt;=</span> <span class="Identifier">k</span> <span class="Keyword">and</span> <span class="Identifier">k</span> <span class="Operator">&lt;=</span> <span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Operator">.</span><span class="Punctuation">}</span>
    <span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="Identifier">forall</span><span class="Punctuation">(</span><span class="Identifier">j</span> <span class="Keyword">in</span> <span class="FloatNumber">1.</span><span class="Operator">.&lt;</span><span class="Identifier">k</span><span class="Punctuation">,</span> <span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">0.</span><span class="Operator">.&lt;</span><span class="Identifier">j</span><span class="Punctuation">,</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span> <span class="Operator">&lt;=</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">j</span><span class="Punctuation">]</span><span class="Punctuation">)</span><span class="Operator">.</span><span class="Punctuation">}</span>
    <span class="Keyword">var</span> <span class="Identifier">t</span> <span class="Operator">=</span> <span class="Identifier">k</span>
    <span class="Keyword">while</span> <span class="Identifier">t</span> <span class="Operator">&gt;</span> <span class="DecNumber">0</span> <span class="Keyword">and</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">t</span><span class="Operator">-</span><span class="DecNumber">1</span><span class="Punctuation">]</span> <span class="Operator">&gt;</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">t</span><span class="Punctuation">]</span><span class="Punctuation">:</span>
      <span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="Identifier">k</span> <span class="Operator">&lt;</span> <span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Operator">.</span><span class="Punctuation">}</span>
      <span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="DecNumber">0</span> <span class="Operator">&lt;=</span> <span class="Identifier">t</span> <span class="Keyword">and</span> <span class="Identifier">t</span> <span class="Operator">&lt;=</span> <span class="Identifier">k</span><span class="Operator">.</span><span class="Punctuation">}</span>
      <span class="Punctuation">{</span><span class="Operator">.</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="Identifier">forall</span><span class="Punctuation">(</span><span class="Identifier">j</span> <span class="Keyword">in</span> <span class="FloatNumber">1.</span><span class="Operator">.</span><span class="Identifier">k</span><span class="Punctuation">,</span> <span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">0.</span><span class="Operator">.&lt;</span><span class="Identifier">j</span><span class="Punctuation">,</span> <span class="Identifier">j</span> <span class="Operator">==</span> <span class="Identifier">t</span> <span class="Keyword">or</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span> <span class="Operator">&lt;=</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">j</span><span class="Punctuation">]</span><span class="Punctuation">)</span><span class="Operator">.</span><span class="Punctuation">}</span>
      <span class="Identifier">swap</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">t</span><span class="Punctuation">]</span><span class="Punctuation">,</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">t</span><span class="Operator">-</span><span class="DecNumber">1</span><span class="Punctuation">]</span>
      <span class="Identifier">dec</span> <span class="Identifier">t</span></pre></p>
<p>Unfortunately, the invariants required to prove that this code is correct take more code than the imperative instructions. However, this effort can be compensated by the fact that the result needs very little testing. Be aware though that DrNim only proves that after <tt class="docutils literal"><span class="pre"><span class="Identifier">insertionSort</span></span></tt> this condition holds:</p>
<pre>forall(i in 1..&lt;a.len, a[i-1] &lt;= a[i])</pre>
<p>This is required, but not sufficient to describe that a <tt class="docutils literal"><span class="pre"><span class="Identifier">sort</span></span></tt> operation was performed. For example, the same postcondition is true for this proc which doesn't sort at all:</p>
<p><pre class="listing"><span class="Keyword">import</span> <span class="Identifier">std</span> <span class="Operator">/</span> <span class="Identifier">logic</span>

<span class="Keyword">proc</span> <span class="Identifier">insertionSort</span><span class="Punctuation">(</span><span class="Identifier">a</span><span class="Punctuation">:</span> <span class="Keyword">var</span> <span class="Identifier">openArray</span><span class="Punctuation">[</span><span class="Identifier">int</span><span class="Punctuation">]</span><span class="Punctuation">)</span> <span class="Punctuation">{</span><span class="Operator">.</span>
    <span class="Identifier">ensures</span><span class="Punctuation">:</span> <span class="Identifier">forall</span><span class="Punctuation">(</span><span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">1.</span><span class="Operator">.&lt;</span><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Punctuation">,</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Operator">-</span><span class="DecNumber">1</span><span class="Punctuation">]</span> <span class="Operator">&lt;=</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span><span class="Punctuation">)</span><span class="Operator">.</span><span class="Punctuation">}</span> <span class="Operator">=</span>
  <span class="Comment"># does not sort, overwrites `a`'s contents!</span>
  <span class="Keyword">for</span> <span class="Identifier">i</span> <span class="Keyword">in</span> <span class="FloatNumber">0.</span><span class="Operator">.&lt;</span><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span><span class="Punctuation">:</span> <span class="Identifier">a</span><span class="Punctuation">[</span><span class="Identifier">i</span><span class="Punctuation">]</span> <span class="Operator">=</span> <span class="Identifier">i</span></pre></p>

<h1><a class="toc-backref" id="syntax-of-propositions" href="#syntax-of-propositions">Syntax of propositions</a></h1><p>The basic syntax is <tt class="docutils literal"><span class="pre"><span class="Identifier">ensures</span><span class="Operator">|</span><span class="Identifier">requires</span><span class="Operator">|</span><span class="Identifier">invariant</span><span class="Punctuation">:</span> <span class="Operator">&lt;</span><span class="Identifier">prop</span><span class="Operator">&gt;</span></span></tt>. A <tt class="docutils literal"><span class="pre"><span class="Identifier">prop</span></span></tt> is either a comparison or a compound:</p>
<pre>prop = nim_bool_expression
     | prop 'and' prop
     | prop 'or' prop
     | prop '-&gt;' prop # implication
     | prop '&lt;-&gt;' prop
     | 'not' prop
     | '(' prop ')' # you can group props via ()
     | forallProp
     | existsProp

forallProp = 'forall' '(' quantifierList ',' prop ')'
existsProp = 'exists' '(' quantifierList ',' prop ')'

quantifierList = quantifier (',' quantifier)*
quantifier = &lt;new identifier&gt; 'in' nim_iteration_expression</pre>
<p><tt class="docutils literal"><span class="pre"><span class="Identifier">nim_iteration_expression</span></span></tt> here is an ordinary expression of Nim code that describes an iteration space, for example <tt class="docutils literal"><span class="pre"><span class="FloatNumber">1.</span><span class="Operator">.</span><span class="DecNumber">4</span></span></tt> or <tt class="docutils literal"><span class="pre"><span class="FloatNumber">1.</span><span class="Operator">.&lt;</span><span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span></span></tt>.</p>
<p><tt class="docutils literal"><span class="pre"><span class="Identifier">nim_bool_expression</span></span></tt> here is an ordinary expression of Nim code of type <tt class="docutils literal"><span class="pre"><span class="Identifier">bool</span></span></tt> like <tt class="docutils literal"><span class="pre"><span class="Identifier">a</span> <span class="Operator">==</span> <span class="DecNumber">3</span></span></tt> or <tt class="docutils literal"><span class="pre"><span class="DecNumber">23</span> <span class="Operator">&gt;</span> <span class="Identifier">a</span><span class="Operator">.</span><span class="Identifier">len</span></span></tt>.</p>
<p>The supported subset of Nim code that can be used in these expressions is currently underspecified but <tt class="docutils literal"><span class="pre"><span class="Keyword">let</span></span></tt> variables, function parameters and <tt class="docutils literal"><span class="pre"><span class="Identifier">result</span></span></tt> (which represents the function's final result) are amenable for verification. The expressions must not have any side-effects and must terminate.</p>
<p>The operators <tt class="docutils literal"><span class="pre"><span class="Identifier">forall</span></span></tt>, <tt class="docutils literal"><span class="pre"><span class="Identifier">exists</span></span></tt>, <tt class="docutils literal"><span class="pre"><span class="Operator">-&gt;</span></span></tt>, <tt class="docutils literal"><span class="pre"><span class="Operator">&lt;-&gt;</span></span></tt> have to imported from <tt class="docutils literal"><span class="pre"><span class="Identifier">std</span> <span class="Operator">/</span> <span class="Identifier">logic</span></span></tt>. </p>
</p>
    
  </div>
</div>

      <div class="twelve-columns footer">
        <span class="nim-sprite"></span>
        <br>
        <small style="color: var(--hint);">Made with Nim. Generated: 2025-01-09 11:59:35 UTC</small>
      </div>
    </div>
  </div>
      <script defer data-domain="nim-lang.org" src="https://plausible.io/js/plausible.js"></script>
    
</body>
</html>