528 lines
35 KiB
HTML
528 lines
35 KiB
HTML
|
||
<!DOCTYPE html>
|
||
<html lang="en">
|
||
<head>
|
||
<meta charset="utf-8">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1.0">
|
||
<meta name="color-scheme" content="light dark">
|
||
<title>PEP 316 – Programming by Contract for Python | peps.python.org</title>
|
||
<link rel="shortcut icon" href="../_static/py.png">
|
||
<link rel="canonical" href="https://peps.python.org/pep-0316/">
|
||
<link rel="stylesheet" href="../_static/style.css" type="text/css">
|
||
<link rel="stylesheet" href="../_static/mq.css" type="text/css">
|
||
<link rel="stylesheet" href="../_static/pygments.css" type="text/css" media="(prefers-color-scheme: light)" id="pyg-light">
|
||
<link rel="stylesheet" href="../_static/pygments_dark.css" type="text/css" media="(prefers-color-scheme: dark)" id="pyg-dark">
|
||
<link rel="alternate" type="application/rss+xml" title="Latest PEPs" href="https://peps.python.org/peps.rss">
|
||
<meta property="og:title" content='PEP 316 – Programming by Contract for Python | peps.python.org'>
|
||
<meta property="og:description" content="This submission describes programming by contract for Python. Eiffel’s Design By Contract(tm) is perhaps the most popular use of programming contracts 2.">
|
||
<meta property="og:type" content="website">
|
||
<meta property="og:url" content="https://peps.python.org/pep-0316/">
|
||
<meta property="og:site_name" content="Python Enhancement Proposals (PEPs)">
|
||
<meta property="og:image" content="https://peps.python.org/_static/og-image.png">
|
||
<meta property="og:image:alt" content="Python PEPs">
|
||
<meta property="og:image:width" content="200">
|
||
<meta property="og:image:height" content="200">
|
||
<meta name="description" content="This submission describes programming by contract for Python. Eiffel’s Design By Contract(tm) is perhaps the most popular use of programming contracts 2.">
|
||
<meta name="theme-color" content="#3776ab">
|
||
</head>
|
||
<body>
|
||
|
||
<svg xmlns="http://www.w3.org/2000/svg" style="display: none;">
|
||
<symbol id="svg-sun-half" viewBox="0 0 24 24" pointer-events="all">
|
||
<title>Following system colour scheme</title>
|
||
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none"
|
||
stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round">
|
||
<circle cx="12" cy="12" r="9"></circle>
|
||
<path d="M12 3v18m0-12l4.65-4.65M12 14.3l7.37-7.37M12 19.6l8.85-8.85"></path>
|
||
</svg>
|
||
</symbol>
|
||
<symbol id="svg-moon" viewBox="0 0 24 24" pointer-events="all">
|
||
<title>Selected dark colour scheme</title>
|
||
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none"
|
||
stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round">
|
||
<path stroke="none" d="M0 0h24v24H0z" fill="none"></path>
|
||
<path d="M12 3c.132 0 .263 0 .393 0a7.5 7.5 0 0 0 7.92 12.446a9 9 0 1 1 -8.313 -12.454z"></path>
|
||
</svg>
|
||
</symbol>
|
||
<symbol id="svg-sun" viewBox="0 0 24 24" pointer-events="all">
|
||
<title>Selected light colour scheme</title>
|
||
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24" fill="none"
|
||
stroke="currentColor" stroke-width="2" stroke-linecap="round" stroke-linejoin="round">
|
||
<circle cx="12" cy="12" r="5"></circle>
|
||
<line x1="12" y1="1" x2="12" y2="3"></line>
|
||
<line x1="12" y1="21" x2="12" y2="23"></line>
|
||
<line x1="4.22" y1="4.22" x2="5.64" y2="5.64"></line>
|
||
<line x1="18.36" y1="18.36" x2="19.78" y2="19.78"></line>
|
||
<line x1="1" y1="12" x2="3" y2="12"></line>
|
||
<line x1="21" y1="12" x2="23" y2="12"></line>
|
||
<line x1="4.22" y1="19.78" x2="5.64" y2="18.36"></line>
|
||
<line x1="18.36" y1="5.64" x2="19.78" y2="4.22"></line>
|
||
</svg>
|
||
</symbol>
|
||
</svg>
|
||
<script>
|
||
|
||
document.documentElement.dataset.colour_scheme = localStorage.getItem("colour_scheme") || "auto"
|
||
</script>
|
||
<section id="pep-page-section">
|
||
<header>
|
||
<h1>Python Enhancement Proposals</h1>
|
||
<ul class="breadcrumbs">
|
||
<li><a href="https://www.python.org/" title="The Python Programming Language">Python</a> » </li>
|
||
<li><a href="../pep-0000/">PEP Index</a> » </li>
|
||
<li>PEP 316</li>
|
||
</ul>
|
||
<button id="colour-scheme-cycler" onClick="setColourScheme(nextColourScheme())">
|
||
<svg aria-hidden="true" class="colour-scheme-icon-when-auto"><use href="#svg-sun-half"></use></svg>
|
||
<svg aria-hidden="true" class="colour-scheme-icon-when-dark"><use href="#svg-moon"></use></svg>
|
||
<svg aria-hidden="true" class="colour-scheme-icon-when-light"><use href="#svg-sun"></use></svg>
|
||
<span class="visually-hidden">Toggle light / dark / auto colour theme</span>
|
||
</button>
|
||
</header>
|
||
<article>
|
||
<section id="pep-content">
|
||
<h1 class="page-title">PEP 316 – Programming by Contract for Python</h1>
|
||
<dl class="rfc2822 field-list simple">
|
||
<dt class="field-odd">Author<span class="colon">:</span></dt>
|
||
<dd class="field-odd">Terence Way <terry at wayforward.net></dd>
|
||
<dt class="field-even">Status<span class="colon">:</span></dt>
|
||
<dd class="field-even"><abbr title="Inactive draft that may be taken up again at a later time">Deferred</abbr></dd>
|
||
<dt class="field-odd">Type<span class="colon">:</span></dt>
|
||
<dd class="field-odd"><abbr title="Normative PEP with a new feature for Python, implementation change for CPython or interoperability standard for the ecosystem">Standards Track</abbr></dd>
|
||
<dt class="field-even">Created<span class="colon">:</span></dt>
|
||
<dd class="field-even">02-May-2003</dd>
|
||
<dt class="field-odd">Post-History<span class="colon">:</span></dt>
|
||
<dd class="field-odd"><p></p></dd>
|
||
</dl>
|
||
<hr class="docutils" />
|
||
<section id="contents">
|
||
<details><summary>Table of Contents</summary><ul class="simple">
|
||
<li><a class="reference internal" href="#abstract">Abstract</a></li>
|
||
<li><a class="reference internal" href="#motivation">Motivation</a></li>
|
||
<li><a class="reference internal" href="#specification">Specification</a><ul>
|
||
<li><a class="reference internal" href="#exceptions">Exceptions</a></li>
|
||
<li><a class="reference internal" href="#inheritance">Inheritance</a></li>
|
||
</ul>
|
||
</li>
|
||
<li><a class="reference internal" href="#rationale">Rationale</a></li>
|
||
<li><a class="reference internal" href="#reference-implementation">Reference Implementation</a></li>
|
||
<li><a class="reference internal" href="#references">References</a></li>
|
||
<li><a class="reference internal" href="#copyright">Copyright</a></li>
|
||
</ul>
|
||
</details></section>
|
||
<section id="abstract">
|
||
<h2><a class="toc-backref" href="#abstract" role="doc-backlink">Abstract</a></h2>
|
||
<p>This submission describes programming by contract for Python.
|
||
Eiffel’s Design By Contract(tm) is perhaps the most popular use of
|
||
programming contracts <a class="footnote-reference brackets" href="#dbc" id="id1">[2]</a>.</p>
|
||
<p>Programming contracts extends the language to include invariant
|
||
expressions for classes and modules, and pre- and post-condition
|
||
expressions for functions and methods.</p>
|
||
<p>These expressions (contracts) are similar to assertions: they must be
|
||
true or the program is stopped, and run-time checking of the contracts
|
||
is typically only enabled while debugging. Contracts are higher-level
|
||
than straight assertions and are typically included in documentation.</p>
|
||
</section>
|
||
<section id="motivation">
|
||
<h2><a class="toc-backref" href="#motivation" role="doc-backlink">Motivation</a></h2>
|
||
<p>Python already has assertions, why add extra stuff to the language to
|
||
support something like contracts? The two best reasons are 1) better,
|
||
more accurate documentation, and 2) easier testing.</p>
|
||
<p>Complex modules and classes never seem to be documented quite right.
|
||
The documentation provided may be enough to convince a programmer to
|
||
use a particular module or class over another, but the programmer
|
||
almost always has to read the source code when the real debugging
|
||
starts.</p>
|
||
<p>Contracts extend the excellent example provided by the <code class="docutils literal notranslate"><span class="pre">doctest</span></code>
|
||
module <a class="footnote-reference brackets" href="#doctest" id="id2">[4]</a>. Documentation is readable by programmers, yet has
|
||
executable tests embedded in it.</p>
|
||
<p>Testing code with contracts is easier too. Comprehensive contracts
|
||
are equivalent to unit tests <a class="footnote-reference brackets" href="#xp" id="id3">[8]</a>. Tests exercise the full range of
|
||
pre-conditions, and fail if the post-conditions are triggered.
|
||
Theoretically, a correctly specified function can be tested completely
|
||
randomly.</p>
|
||
<p>So why add this to the language? Why not have several different
|
||
implementations, or let programmers implement their own assertions?
|
||
The answer is the behavior of contracts under inheritance.</p>
|
||
<p>Suppose Alice and Bob use different assertions packages. If Alice
|
||
produces a class library protected by assertions, Bob cannot derive
|
||
classes from Alice’s library and expect proper checking of
|
||
post-conditions and invariants. If they both use the same assertions
|
||
package, then Bob can override Alice’s methods yet still test against
|
||
Alice’s contract assertions. The natural place to find this
|
||
assertions system is in the language’s run-time library.</p>
|
||
</section>
|
||
<section id="specification">
|
||
<h2><a class="toc-backref" href="#specification" role="doc-backlink">Specification</a></h2>
|
||
<p>The docstring of any module or class can include invariant contracts
|
||
marked off with a line that starts with the keyword <code class="docutils literal notranslate"><span class="pre">inv</span></code> followed
|
||
by a colon (:). Whitespace at the start of the line and around the
|
||
colon is ignored. The colon is either immediately followed by a
|
||
single expression on the same line, or by a series of expressions on
|
||
following lines indented past the <code class="docutils literal notranslate"><span class="pre">inv</span></code> keyword. The normal Python
|
||
rules about implicit and explicit line continuations are followed
|
||
here. Any number of invariant contracts can be in a docstring.</p>
|
||
<p>Some examples:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="c1"># state enumeration</span>
|
||
<span class="n">START</span><span class="p">,</span> <span class="n">CONNECTING</span><span class="p">,</span> <span class="n">CONNECTED</span><span class="p">,</span> <span class="n">CLOSING</span><span class="p">,</span> <span class="n">CLOSED</span> <span class="o">=</span> <span class="nb">range</span><span class="p">(</span><span class="mi">5</span><span class="p">)</span>
|
||
|
||
<span class="k">class</span><span class="w"> </span><span class="nc">conn</span><span class="p">:</span>
|
||
|
||
<span class="w"> </span><span class="sd">"""A network connection</span>
|
||
|
||
<span class="sd"> inv: self.state in [START, CLOSED, # closed states</span>
|
||
<span class="sd"> CONNECTING, CLOSING, # transition states</span>
|
||
<span class="sd"> CONNECTED]</span>
|
||
|
||
<span class="sd"> inv: 0 <= self.seqno < 256</span>
|
||
<span class="sd"> """</span>
|
||
|
||
<span class="k">class</span><span class="w"> </span><span class="nc">circbuf</span><span class="p">:</span>
|
||
|
||
<span class="w"> </span><span class="sd">"""A circular buffer.</span>
|
||
|
||
<span class="sd"> inv:</span>
|
||
<span class="sd"> # there can be from 0 to max items on the buffer</span>
|
||
<span class="sd"> 0 <= self.len <= len(self.buf)</span>
|
||
|
||
<span class="sd"> # g is a valid index into buf</span>
|
||
<span class="sd"> 0 <= self.g < len(self.buf)</span>
|
||
|
||
<span class="sd"> # p is also a valid index into buf</span>
|
||
<span class="sd"> 0 <= self.p < len(self.buf)</span>
|
||
|
||
<span class="sd"> # there are len items between get and put</span>
|
||
<span class="sd"> (self.p - self.g) % len(self.buf) == \</span>
|
||
<span class="sd"> self.len % len(self.buf)</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>Module invariants must be true after the module is loaded, and at the
|
||
entry and exit of every public function within the module.</p>
|
||
<p>Class invariants must be true after the <code class="docutils literal notranslate"><span class="pre">__init__</span></code> function returns,
|
||
at the entry of the <code class="docutils literal notranslate"><span class="pre">__del__</span></code> function, and at the entry and exit of
|
||
every other public method of the class. Class invariants must use the
|
||
self variable to access instance variables.</p>
|
||
<p>A method or function is public if its name doesn’t start with an
|
||
underscore (_), unless it starts and ends with ‘__’ (two underscores).</p>
|
||
<p>The docstring of any function or method can have pre-conditions
|
||
documented with the keyword <code class="docutils literal notranslate"><span class="pre">pre</span></code> following the same rules above.
|
||
Post-conditions are documented with the keyword <code class="docutils literal notranslate"><span class="pre">post</span></code> optionally
|
||
followed by a list of variables. The variables are in the same scope
|
||
as the body of the function or method. This list declares the
|
||
variables that the function/method is allowed to modify.</p>
|
||
<p>An example:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">class</span><span class="w"> </span><span class="nc">circbuf</span><span class="p">:</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="fm">__init__</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">leng</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Construct an empty circular buffer.</span>
|
||
|
||
<span class="sd"> pre: leng > 0</span>
|
||
<span class="sd"> post[self]:</span>
|
||
<span class="sd"> self.is_empty()</span>
|
||
<span class="sd"> len(self.buf) == leng</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>A double-colon (::) can be used instead of a single colon (:) to
|
||
support docstrings written using reStructuredText <a class="footnote-reference brackets" href="#rst" id="id4">[7]</a>. For
|
||
example, the following two docstrings describe the same contract:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="sd">"""pre: leng > 0"""</span>
|
||
<span class="sd">"""pre:: leng > 0"""</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>Expressions in pre- and post-conditions are defined in the module
|
||
namespace – they have access to nearly all the variables that the
|
||
function can access, except closure variables.</p>
|
||
<p>The contract expressions in post-conditions have access to two
|
||
additional variables: <code class="docutils literal notranslate"><span class="pre">__old__</span></code> which is filled with shallow copies
|
||
of values declared in the variable list immediately following the post
|
||
keyword, and <code class="docutils literal notranslate"><span class="pre">__return__</span></code> which is bound to the return value of the
|
||
function or method.</p>
|
||
<p>An example:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">class</span><span class="w"> </span><span class="nc">circbuf</span><span class="p">:</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">get</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Pull an entry from a non-empty circular buffer.</span>
|
||
|
||
<span class="sd"> pre: not self.is_empty()</span>
|
||
<span class="sd"> post[self.g, self.len]:</span>
|
||
<span class="sd"> __return__ == self.buf[__old__.self.g]</span>
|
||
<span class="sd"> self.len == __old__.self.len - 1</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>All contract expressions have access to some additional convenience
|
||
functions. To make evaluating the truth of sequences easier, two
|
||
functions <code class="docutils literal notranslate"><span class="pre">forall</span></code> and <code class="docutils literal notranslate"><span class="pre">exists</span></code> are defined as:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span><span class="w"> </span><span class="nf">forall</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">fn</span> <span class="o">=</span> <span class="nb">bool</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Return True only if all elements in a are true.</span>
|
||
|
||
<span class="sd"> >>> forall([])</span>
|
||
<span class="sd"> 1</span>
|
||
<span class="sd"> >>> even = lambda x: x % 2 == 0</span>
|
||
<span class="sd"> >>> forall([2, 4, 6, 8], even)</span>
|
||
<span class="sd"> 1</span>
|
||
<span class="sd"> >>> forall('this is a test'.split(), lambda x: len(x) == 4)</span>
|
||
<span class="sd"> 0</span>
|
||
<span class="sd"> """</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">exists</span><span class="p">(</span><span class="n">a</span><span class="p">,</span> <span class="n">fn</span> <span class="o">=</span> <span class="nb">bool</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Returns True if there is at least one true value in a.</span>
|
||
|
||
<span class="sd"> >>> exists([])</span>
|
||
<span class="sd"> 0</span>
|
||
<span class="sd"> >>> exists('this is a test'.split(), lambda x: len(x) == 4)</span>
|
||
<span class="sd"> 1</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>An example:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">def</span><span class="w"> </span><span class="nf">sort</span><span class="p">(</span><span class="n">a</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Sort a list.</span>
|
||
|
||
<span class="sd"> pre: isinstance(a, type(list))</span>
|
||
<span class="sd"> post[a]:</span>
|
||
<span class="sd"> # array size is unchanged</span>
|
||
<span class="sd"> len(a) == len(__old__.a)</span>
|
||
|
||
<span class="sd"> # array is ordered</span>
|
||
<span class="sd"> forall([a[i] >= a[i-1] for i in range(1, len(a))])</span>
|
||
|
||
<span class="sd"> # all the old elements are still in the array</span>
|
||
<span class="sd"> forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>To make evaluating conditions easier, the function <code class="docutils literal notranslate"><span class="pre">implies</span></code> is
|
||
defined. With two arguments, this is similar to the logical implies
|
||
(=>) operator. With three arguments, this is similar to C’s
|
||
conditional expression (x?a:b). This is defined as:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">implies</span><span class="p">(</span><span class="kc">False</span><span class="p">,</span> <span class="n">a</span><span class="p">)</span> <span class="o">=></span> <span class="kc">True</span>
|
||
<span class="n">implies</span><span class="p">(</span><span class="kc">True</span><span class="p">,</span> <span class="n">a</span><span class="p">)</span> <span class="o">=></span> <span class="n">a</span>
|
||
<span class="n">implies</span><span class="p">(</span><span class="kc">False</span><span class="p">,</span> <span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">)</span> <span class="o">=></span> <span class="n">b</span>
|
||
<span class="n">implies</span><span class="p">(</span><span class="kc">True</span><span class="p">,</span> <span class="n">a</span><span class="p">,</span> <span class="n">b</span><span class="p">)</span> <span class="o">=></span> <span class="n">a</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>On entry to a function, the function’s pre-conditions are checked. An
|
||
assertion error is raised if any pre-condition is false. If the
|
||
function is public, then the class or module’s invariants are also
|
||
checked. Copies of variables declared in the post are saved, the
|
||
function is called, and if the function exits without raising an
|
||
exception, the post-conditions are checked.</p>
|
||
<section id="exceptions">
|
||
<h3><a class="toc-backref" href="#exceptions" role="doc-backlink">Exceptions</a></h3>
|
||
<p>Class/module invariants are checked even if a function or method exits
|
||
by signalling an exception (post-conditions are not).</p>
|
||
<p>All failed contracts raise exceptions which are subclasses of the
|
||
<code class="docutils literal notranslate"><span class="pre">ContractViolationError</span></code> exception, which is in turn a subclass of the
|
||
<code class="docutils literal notranslate"><span class="pre">AssertionError</span></code> exception. Failed pre-conditions raise a
|
||
<code class="docutils literal notranslate"><span class="pre">PreconditionViolationError</span></code> exception. Failed post-conditions raise
|
||
a <code class="docutils literal notranslate"><span class="pre">PostconditionViolationError</span></code> exception, and failed invariants raise
|
||
a <code class="docutils literal notranslate"><span class="pre">InvariantViolationError</span></code> exception.</p>
|
||
<p>The class hierarchy:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="ne">AssertionError</span>
|
||
<span class="n">ContractViolationError</span>
|
||
<span class="n">PreconditionViolationError</span>
|
||
<span class="n">PostconditionViolationError</span>
|
||
<span class="n">InvariantViolationError</span>
|
||
<span class="n">InvalidPreconditionError</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>The <code class="docutils literal notranslate"><span class="pre">InvalidPreconditionError</span></code> is raised when pre-conditions are
|
||
illegally strengthened, see the next section on Inheritance.</p>
|
||
<p>Example:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">try</span><span class="p">:</span>
|
||
<span class="n">some_func</span><span class="p">()</span>
|
||
<span class="k">except</span> <span class="n">contract</span><span class="o">.</span><span class="n">PreconditionViolationError</span><span class="p">:</span>
|
||
<span class="c1"># failed pre-condition, ok</span>
|
||
<span class="k">pass</span>
|
||
</pre></div>
|
||
</div>
|
||
</section>
|
||
<section id="inheritance">
|
||
<h3><a class="toc-backref" href="#inheritance" role="doc-backlink">Inheritance</a></h3>
|
||
<p>A class’s invariants include all the invariants for all super-classes
|
||
(class invariants are ANDed with super-class invariants). These
|
||
invariants are checked in method-resolution order.</p>
|
||
<p>A method’s post-conditions also include all overridden post-conditions
|
||
(method post-conditions are ANDed with all overridden method
|
||
post-conditions).</p>
|
||
<p>An overridden method’s pre-conditions can be ignored if the overriding
|
||
method’s pre-conditions are met. However, if the overriding method’s
|
||
pre-conditions fail, <em>all</em> of the overridden method’s pre-conditions
|
||
must also fail. If not, a separate exception is raised, the
|
||
InvalidPreconditionError. This supports weakening pre-conditions.</p>
|
||
<p>A somewhat contrived example:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="k">class</span><span class="w"> </span><span class="nc">SimpleMailClient</span><span class="p">:</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">send</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">msg</span><span class="p">,</span> <span class="n">dest</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Sends a message to a destination:</span>
|
||
|
||
<span class="sd"> pre: self.is_open() # we must have an open connection</span>
|
||
<span class="sd"> """</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">recv</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Gets the next unread mail message.</span>
|
||
|
||
<span class="sd"> Returns None if no message is available.</span>
|
||
|
||
<span class="sd"> pre: self.is_open() # we must have an open connection</span>
|
||
<span class="sd"> post: __return__ is None or isinstance(__return__, Message)</span>
|
||
<span class="sd"> """</span>
|
||
|
||
<span class="k">class</span><span class="w"> </span><span class="nc">ComplexMailClient</span><span class="p">(</span><span class="n">SimpleMailClient</span><span class="p">):</span>
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">send</span><span class="p">(</span><span class="bp">self</span><span class="p">,</span> <span class="n">msg</span><span class="p">,</span> <span class="n">dest</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Sends a message to a destination.</span>
|
||
|
||
<span class="sd"> The message is sent immediately if currently connected.</span>
|
||
<span class="sd"> Otherwise, the message is queued locally until a</span>
|
||
<span class="sd"> connection is made.</span>
|
||
|
||
<span class="sd"> pre: True # weakens the pre-condition from SimpleMailClient</span>
|
||
<span class="sd"> """</span>
|
||
|
||
<span class="k">def</span><span class="w"> </span><span class="nf">recv</span><span class="p">(</span><span class="bp">self</span><span class="p">):</span>
|
||
<span class="w"> </span><span class="sd">"""Gets the next unread mail message.</span>
|
||
|
||
<span class="sd"> Waits until a message is available.</span>
|
||
|
||
<span class="sd"> pre: True # can always be called</span>
|
||
<span class="sd"> post: isinstance(__return__, Message)</span>
|
||
<span class="sd"> """</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>Because pre-conditions can only be weakened, a <code class="docutils literal notranslate"><span class="pre">ComplexMailClient</span></code> can
|
||
replace a <code class="docutils literal notranslate"><span class="pre">SimpleMailClient</span></code> with no fear of breaking existing code.</p>
|
||
</section>
|
||
</section>
|
||
<section id="rationale">
|
||
<h2><a class="toc-backref" href="#rationale" role="doc-backlink">Rationale</a></h2>
|
||
<p>Except for the following differences, programming-by-contract for
|
||
Python mirrors the Eiffel DBC specification <a class="footnote-reference brackets" href="#oosc" id="id5">[3]</a>.</p>
|
||
<p>Embedding contracts in docstrings is patterned after the doctest
|
||
module. It removes the need for extra syntax, ensures that programs
|
||
with contracts are backwards-compatible, and no further work is
|
||
necessary to have the contracts included in the docs.</p>
|
||
<p>The keywords <code class="docutils literal notranslate"><span class="pre">pre</span></code>, <code class="docutils literal notranslate"><span class="pre">post</span></code>, and <code class="docutils literal notranslate"><span class="pre">inv</span></code> were chosen instead of the
|
||
Eiffel-style <code class="docutils literal notranslate"><span class="pre">REQUIRE</span></code>, <code class="docutils literal notranslate"><span class="pre">ENSURE</span></code>, and <code class="docutils literal notranslate"><span class="pre">INVARIANT</span></code> because
|
||
they’re shorter, more in line with mathematical notation, and for a
|
||
more subtle reason: the word ‘require’ implies caller
|
||
responsibilities, while ‘ensure’ implies provider guarantees. Yet
|
||
pre-conditions can fail through no fault of the caller when using
|
||
multiple inheritance, and post-conditions can fail through no fault of
|
||
the function when using multiple threads.</p>
|
||
<p>Loop invariants as used in Eiffel are unsupported. They’re a pain to
|
||
implement, and not part of the documentation anyway.</p>
|
||
<p>The variable names <code class="docutils literal notranslate"><span class="pre">__old__</span></code> and <code class="docutils literal notranslate"><span class="pre">__return__</span></code> were picked to avoid
|
||
conflicts with the <code class="docutils literal notranslate"><span class="pre">return</span></code> keyword and to stay consistent with
|
||
Python naming conventions: they’re public and provided by the Python
|
||
implementation.</p>
|
||
<p>Having variable declarations after a post keyword describes exactly
|
||
what the function or method is allowed to modify. This removes the
|
||
need for the <code class="docutils literal notranslate"><span class="pre">NoChange</span></code> syntax in Eiffel, and makes the
|
||
implementation of <code class="docutils literal notranslate"><span class="pre">__old__</span></code> much easier. It also is more in line
|
||
with Z schemas <a class="footnote-reference brackets" href="#z" id="id6">[9]</a>, which are divided into two parts: declaring what
|
||
changes followed by limiting the changes.</p>
|
||
<p>Shallow copies of variables for the <code class="docutils literal notranslate"><span class="pre">__old__</span></code> value prevent an
|
||
implementation of contract programming from slowing down a system too
|
||
much. If a function changes values that wouldn’t be caught by a
|
||
shallow copy, it can declare the changes like so:</p>
|
||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">post</span><span class="p">[</span><span class="bp">self</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">obj</span><span class="p">,</span> <span class="bp">self</span><span class="o">.</span><span class="n">obj</span><span class="o">.</span><span class="n">p</span><span class="p">]</span>
|
||
</pre></div>
|
||
</div>
|
||
<p>The <code class="docutils literal notranslate"><span class="pre">forall</span></code>, <code class="docutils literal notranslate"><span class="pre">exists</span></code>, and <code class="docutils literal notranslate"><span class="pre">implies</span></code> functions were added after
|
||
spending some time documenting existing functions with contracts.
|
||
These capture a majority of common specification idioms. It might
|
||
seem that defining <code class="docutils literal notranslate"><span class="pre">implies</span></code> as a function might not work (the
|
||
arguments are evaluated whether needed or not, in contrast with other
|
||
boolean operators), but it works for contracts since there should be
|
||
no side-effects for any expression in a contract.</p>
|
||
</section>
|
||
<section id="reference-implementation">
|
||
<h2><a class="toc-backref" href="#reference-implementation" role="doc-backlink">Reference Implementation</a></h2>
|
||
<p>A reference implementation is available <a class="footnote-reference brackets" href="#imp" id="id7">[1]</a>. It replaces existing
|
||
functions with new functions that do contract checking, by directly
|
||
changing the class’ or module’s namespace.</p>
|
||
<p>Other implementations exist that either hack <code class="docutils literal notranslate"><span class="pre">__getattr__</span></code> <a class="footnote-reference brackets" href="#dbc4p" id="id8">[5]</a>
|
||
or use <code class="docutils literal notranslate"><span class="pre">__metaclass__</span></code> <a class="footnote-reference brackets" href="#pydbc" id="id9">[6]</a>.</p>
|
||
</section>
|
||
<section id="references">
|
||
<h2><a class="toc-backref" href="#references" role="doc-backlink">References</a></h2>
|
||
<aside class="footnote-list brackets">
|
||
<aside class="footnote brackets" id="imp" role="doc-footnote">
|
||
<dt class="label" id="imp">[<a href="#id7">1</a>]</dt>
|
||
<dd>Implementation described in this document.
|
||
(<a class="reference external" href="http://www.wayforward.net/pycontract/">http://www.wayforward.net/pycontract/</a>)</aside>
|
||
<aside class="footnote brackets" id="dbc" role="doc-footnote">
|
||
<dt class="label" id="dbc">[<a href="#id1">2</a>]</dt>
|
||
<dd>Design By Contract is a registered trademark of Eiffel
|
||
Software Inc.
|
||
(<a class="reference external" href="http://archive.eiffel.com/doc/manuals/technology/contract/">http://archive.eiffel.com/doc/manuals/technology/contract/</a>)</aside>
|
||
<aside class="footnote brackets" id="oosc" role="doc-footnote">
|
||
<dt class="label" id="oosc">[<a href="#id5">3</a>]</dt>
|
||
<dd>Object-oriented Software Construction, Bertrand Meyer,
|
||
ISBN 0-13-629031-0</aside>
|
||
<aside class="footnote brackets" id="doctest" role="doc-footnote">
|
||
<dt class="label" id="doctest">[<a href="#id2">4</a>]</dt>
|
||
<dd><a class="reference external" href="http://docs.python.org/library/doctest.html">http://docs.python.org/library/doctest.html</a>
|
||
doctest – Test docstrings represent reality</aside>
|
||
<aside class="footnote brackets" id="dbc4p" role="doc-footnote">
|
||
<dt class="label" id="dbc4p">[<a href="#id8">5</a>]</dt>
|
||
<dd>Design by Contract for Python, R. Plosch
|
||
<em>IEEE Proceedings of the Joint Asia Pacific Software Engineering
|
||
Conference (APSEC97/ICSC97), Hong Kong, December 2-5, 1997</em>
|
||
(<a class="reference external" href="http://www.swe.uni-linz.ac.at/publications/abstract/TR-SE-97.24.html">http://www.swe.uni-linz.ac.at/publications/abstract/TR-SE-97.24.html</a>)</aside>
|
||
<aside class="footnote brackets" id="pydbc" role="doc-footnote">
|
||
<dt class="label" id="pydbc">[<a href="#id9">6</a>]</dt>
|
||
<dd>PyDBC – Design by Contract for Python 2.2+,
|
||
Daniel Arbuckle
|
||
(<a class="reference external" href="http://www.nongnu.org/pydbc/">http://www.nongnu.org/pydbc/</a>)</aside>
|
||
<aside class="footnote brackets" id="rst" role="doc-footnote">
|
||
<dt class="label" id="rst">[<a href="#id4">7</a>]</dt>
|
||
<dd>ReStructuredText (<a class="reference external" href="http://docutils.sourceforge.net/rst.html">http://docutils.sourceforge.net/rst.html</a>)</aside>
|
||
<aside class="footnote brackets" id="xp" role="doc-footnote">
|
||
<dt class="label" id="xp">[<a href="#id3">8</a>]</dt>
|
||
<dd>Extreme Programming Explained, Kent Beck,
|
||
ISBN 0-201-61641-6</aside>
|
||
<aside class="footnote brackets" id="z" role="doc-footnote">
|
||
<dt class="label" id="z">[<a href="#id6">9</a>]</dt>
|
||
<dd>The Z Notation, Second Edition, J.M. Spivey
|
||
ISBN 0-13-978529-9</aside>
|
||
</aside>
|
||
</section>
|
||
<section id="copyright">
|
||
<h2><a class="toc-backref" href="#copyright" role="doc-backlink">Copyright</a></h2>
|
||
<p>This document has been placed in the public domain.</p>
|
||
</section>
|
||
</section>
|
||
<hr class="docutils" />
|
||
<p>Source: <a class="reference external" href="https://github.com/python/peps/blob/main/peps/pep-0316.rst">https://github.com/python/peps/blob/main/peps/pep-0316.rst</a></p>
|
||
<p>Last modified: <a class="reference external" href="https://github.com/python/peps/commits/main/peps/pep-0316.rst">2025-02-01 08:59:27 GMT</a></p>
|
||
|
||
</article>
|
||
<nav id="pep-sidebar">
|
||
<h2>Contents</h2>
|
||
<ul>
|
||
<li><a class="reference internal" href="#abstract">Abstract</a></li>
|
||
<li><a class="reference internal" href="#motivation">Motivation</a></li>
|
||
<li><a class="reference internal" href="#specification">Specification</a><ul>
|
||
<li><a class="reference internal" href="#exceptions">Exceptions</a></li>
|
||
<li><a class="reference internal" href="#inheritance">Inheritance</a></li>
|
||
</ul>
|
||
</li>
|
||
<li><a class="reference internal" href="#rationale">Rationale</a></li>
|
||
<li><a class="reference internal" href="#reference-implementation">Reference Implementation</a></li>
|
||
<li><a class="reference internal" href="#references">References</a></li>
|
||
<li><a class="reference internal" href="#copyright">Copyright</a></li>
|
||
</ul>
|
||
|
||
<br>
|
||
<a id="source" href="https://github.com/python/peps/blob/main/peps/pep-0316.rst">Page Source (GitHub)</a>
|
||
</nav>
|
||
</section>
|
||
<script src="../_static/colour_scheme.js"></script>
|
||
<script src="../_static/wrap_tables.js"></script>
|
||
<script src="../_static/sticky_banner.js"></script>
|
||
</body>
|
||
</html> |