|
11 | 11 | <link rel="stylesheet" type="text/css" href="../_static/css/theme.css?v=9edc463e" /> |
12 | 12 | <link rel="stylesheet" type="text/css" href="../_static/proofnav/proofnav.css?v=4392ad40" /> |
13 | 13 | <link rel="stylesheet" type="text/css" href="../_static/sphinx-design.min.css?v=95c83b7e" /> |
| 14 | + <link rel="stylesheet" type="text/css" href="../_static/easycrypt.css?v=38956531" /> |
14 | 15 |
|
15 | 16 |
|
16 | 17 | <script src="../_static/jquery.js?v=5d32c60e"></script> |
|
49 | 50 | <ul class="current"> |
50 | 51 | <li class="toctree-l1 current"><a class="reference internal" href="../tactics.html">Proof tactics reference</a><ul class="current"> |
51 | 52 | <li class="toctree-l2"><a class="reference internal" href="if.html">Tactic: <code class="docutils literal notranslate"><span class="pre">if</span></code></a></li> |
52 | | -<li class="toctree-l2 current"><a class="current reference internal" href="#">Tactic: <cite>skip</cite></a><ul> |
| 53 | +<li class="toctree-l2 current"><a class="current reference internal" href="#">Tactic: <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">skip</span></code></a><ul> |
53 | 54 | <li class="toctree-l3"><a class="reference internal" href="#variant-skip-hl">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (HL)</a></li> |
54 | 55 | <li class="toctree-l3"><a class="reference internal" href="#variant-skip-prhl">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (pRHL)</a></li> |
55 | 56 | <li class="toctree-l3"><a class="reference internal" href="#variant-skip-phl">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (pHL)</a></li> |
|
76 | 77 | <ul class="wy-breadcrumbs"> |
77 | 78 | <li><a href="../index.html" class="icon icon-home" aria-label="Home"></a></li> |
78 | 79 | <li class="breadcrumb-item"><a href="../tactics.html">Proof tactics reference</a></li> |
79 | | - <li class="breadcrumb-item active">Tactic: <cite>skip</cite></li> |
| 80 | + <li class="breadcrumb-item active">Tactic: <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">skip</span></code></li> |
80 | 81 | <li class="wy-breadcrumbs-aside"> |
81 | 82 | <a href="../_sources/tactics/skip.rst.txt" rel="nofollow"> View page source</a> |
82 | 83 | </li> |
|
87 | 88 | <div itemprop="articleBody"> |
88 | 89 |
|
89 | 90 | <section id="tactic-skip"> |
90 | | -<h1>Tactic: <cite>skip</cite><a class="headerlink" href="#tactic-skip" title="Link to this heading"></a></h1> |
| 91 | +<h1>Tactic: <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">skip</span></code><a class="headerlink" href="#tactic-skip" title="Link to this heading"></a></h1> |
91 | 92 | <p>The <code class="docutils literal notranslate"><span class="pre">skip</span></code> tactic applies to program-logic goals where the program(s) |
92 | 93 | under consideration are empty. In this situation, program execution |
93 | 94 | performs no computation and produces no state changes.</p> |
@@ -174,7 +175,7 @@ <h2><a class="toc-backref" href="#id1" role="doc-backlink">Variant: <code class= |
174 | 175 | </section> |
175 | 176 | <section id="variant-skip-prhl"> |
176 | 177 | <h2><a class="toc-backref" href="#id2" role="doc-backlink">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (pRHL)</a><a class="headerlink" href="#variant-skip-prhl" title="Link to this heading"></a></h2> |
177 | | -<p>In the relational Hoare logic setting, the <cite>skip`</cite> tactic applies only |
| 178 | +<p>In the relational Hoare logic setting, the <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">skip</span>`</code> tactic applies only |
178 | 179 | when both programs are empty, in which case it reduces the relational |
179 | 180 | judgment to obligations on the preconditions and postconditions alone.</p> |
180 | 181 |
|
|
0 commit comments