Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Export from org mode to wiki-markdown
- Loading branch information
Showing
4 changed files
with
361 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,213 @@ | ||
contract | ||
======== | ||
|
||
As you saw in the description of [defconstrainedfn] core.contracts | ||
allows you to create functions with a localized and dependent | ||
contract. However, there may be circumstances where the separation of | ||
contract and constrained function is preferred. Take for example, a | ||
simple slope function: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">defn </span><span class="nv">sqr</span> <span | ||
class="p">[</span><span class="nv">n</span><span class="p">]</span> | ||
<span class="p">(</span><span class="nb">* </span><span | ||
class="nv">n</span> <span class="nv">n</span><span | ||
class="p">))</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
Defining a separate contract for this function is a simple matter: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">def </span><span class="nv">sqr-contract</span></div><div | ||
class="line" id="LC2"> <span class="p">(</span><span | ||
class="nf">contract</span> <span | ||
class="nv">sqr-constraints</span></div><div class="line" | ||
id="LC3"> <span class="s">"Defines the | ||
constraints for squaring"</span></div><div class="line" | ||
id="LC4"> <span class="p">[</span><span | ||
class="nv">n</span><span class="p">]</span> <span | ||
class="p">[</span><span class="nv">number?</span> <span | ||
class="p">(</span><span class="nb">not= </span><span | ||
class="mi">0</span> <span class="nv">n</span><span class="p">)</span> | ||
<span class="nv">=></span> <span class="nv">pos?</span> <span | ||
class="nv">number?</span><span class="p">]))</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
We can then define a constrained version of sqr using | ||
core.contracts's [with-constraints] macro: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">def </span><span class="nv">constrained-sqr</span> | ||
</div><div class="line" id="LC2"> <span | ||
class="p">(</span><span class="nf">with-constraints</span></div><div | ||
class="line" id="LC3"> <span | ||
class="nv">sqr</span></div><div class="line" | ||
id="LC4"> <span | ||
class="nv">sqr-contract</span><span class="p">))</span></div><div | ||
class="line" id="LC5"><br/></div><div class="line" id="LC6"><span | ||
class="p">(</span><span class="nf">constrained-sqr</span> <span | ||
class="mi">5</span><span class="p">)</span></div><div class="line" | ||
id="LC7"><span class="c1">;=> 25</span></div><div class="line" | ||
id="LC8"><br/></div><div class="line" id="LC9"><span | ||
class="p">(</span><span class="nf">constrained-sqr</span> <span | ||
class="mi">-5</span><span class="p">)</span></div><div class="line" | ||
id="LC10"><span class="c1">;=> 25</span></div><div class="line" | ||
id="LC11"><br/></div><div class="line" id="LC12"><span | ||
class="p">(</span><span class="nf">constrained-sqr</span> <span | ||
class="mi">0</span><span class="p">)</span></div><div class="line" | ||
id="LC13"><span class="c1">; java.lang.AssertionError: Assert failed: | ||
<br/> (not= 0 num)</span></div><div class="line" | ||
id="LC14"><br/></div><div class="line" id="LC15"><span | ||
class="p">(</span><span class="nf">constrained-sqr</span> <span | ||
class="nv">:a</span><span class="p">)</span></div><div class="line" | ||
id="LC16"><span class="c1">; java.lang.AssertionError: Assert failed: | ||
<br/> (number? num)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
However, this constraint definition for sqr, while accurate, is very | ||
broad. In fact, the software team developing software for the 8-bit | ||
Atari console would not be able to use constrained-sqr as it is far | ||
too liberal. Therefore, they can define their own contract that | ||
further constrains constrained-sqr: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">def </span><span | ||
class="nv">sqr-8bit-contract</span></div><div class="line" | ||
id="LC2"> <span class="p">(</span><span | ||
class="nf">contract</span> <span | ||
class="nv">atari-constraints</span></div><div class="line" | ||
id="LC3"> <span class="s">"Defines the | ||
constraints for Atari 2600 sqr"</span></div><div class="line" | ||
id="LC4"> <span class="p">[</span><span | ||
class="nv">_</span><span class="p">]</span> <span | ||
class="p">[</span><span class="nv">number?</span> <span | ||
class="nv">=></span> <span class="p">(</span><span class="nb">< | ||
</span><span class="nv">%</span> <span class="mi">256</span><span | ||
class="p">)]))</span></div><div class="line" id="LC5"><br/></div><div | ||
class="line" id="LC6"><span class="p">(</span><span class="k">def | ||
</span><span class="nv">sqr-8bit</span></div><div class="line" | ||
id="LC7"> <span class="p">(</span><span | ||
class="nf">with-constraints</span></div><div class="line" | ||
id="LC8"> <span | ||
class="nv">constrained-sqr</span> </div><div class="line" | ||
id="LC9"> <span | ||
class="nv">sqr-8bit-contract</span><span class="p">))</span></div><div | ||
class="line" id="LC10"><br/></div><div class="line" id="LC11"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mi">5</span><span class="p">)</span></div><div class="line" | ||
id="LC12"><span class="c1">;=> 25</span></div><div class="line" | ||
id="LC13"><br/></div><div class="line" id="LC14"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mi">0</span><span class="p">)</span></div><div class="line" | ||
id="LC15"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC16"><span class="c1">; Assert | ||
failed: (not= 0 num)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
And all appears to be in order -- except: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="nf">sqr-8bit</span> <span class="mi">100</span><span | ||
class="p">)</span></div><div class="line" id="LC2"><span class="c1">; | ||
java.lang.AssertionError:</span></div><div class="line" id="LC4"><span | ||
class="c1">; Assert failed: (< % 256)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
That is, calling the function sqr-8bit with 100 causes a | ||
post-condition failure! The reason for this is because the | ||
underlying sqr is the same old arbitrary-precision version when what | ||
we really want is a function that deals in only 8-bit values. There | ||
are two possible ways to do this: | ||
1. Create a version of sqr-8bit that does in fact deal in 8-bit | ||
values | ||
2. Tighten the constraint on constrained-sqr further by applying | ||
another contract | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">def </span><span | ||
class="nv">sqr-8bit-contract</span></div><div class="line" | ||
id="LC2"> <span class="p">(</span><span | ||
class="nf">contract</span> <span | ||
class="nv">atari-constraints</span></div><div class="line" | ||
id="LC3"> <span class="s">"Defines the | ||
constraints for Atari 2600 sqr"</span></div><div class="line" | ||
id="LC4"> <span class="p">[</span><span | ||
class="nv">n</span><span class="p">]</span> <span | ||
class="p">[(</span><span class="nb">< </span><span | ||
class="nv">n</span> <span class="mi">16</span><span class="p">)</span> | ||
<span class="nv">integer?</span> <span class="nv">pos?</span> <span | ||
class="nv">=></span> <span class="p">(</span><span class="nb">< | ||
</span><span class="nv">%</span> <span class="mi">256</span><span | ||
class="p">)]))</span></div><div class="line" id="LC5"><br/></div><div | ||
class="line" id="LC6"><span class="p">(</span><span class="k">def | ||
</span><span class="nv">sqr-8bit</span></div><div class="line" | ||
id="LC7"> <span class="p">(</span><span | ||
class="nf">with-constraints</span></div><div class="line" | ||
id="LC8"> <span | ||
class="nv">constrained-sqr</span> </div><div class="line" | ||
id="LC9"> <span | ||
class="nv">sqr-8bit-contract</span><span class="p">))</span></div><div | ||
class="line" id="LC10"><br/></div><div class="line" id="LC12"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mi">15</span><span class="p">)</span></div><div class="line" | ||
id="LC13"><span class="c1">;=> 225</span></div><div class="line" | ||
id="LC14"><br/></div><div class="line" id="LC15"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mi">-5</span><span class="p">)</span></div><div class="line" | ||
id="LC16"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC17"><span class="c1">; Assert | ||
failed: (pos? n)</span></div><div class="line" | ||
id="LC18"><br/></div><div class="line" id="LC19"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mf">15.9687194</span><span class="p">)</span></div><div | ||
class="line" id="LC20"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC21"><span class="c1">; Assert | ||
failed: (integer? n)</span></div><div class="line" | ||
id="LC22"><br/></div><div class="line" id="LC23"><span | ||
class="p">(</span><span class="nf">sqr-8bit</span> <span | ||
class="mi">16</span><span class="p">)</span></div><div class="line" | ||
id="LC24"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC25"><span class="c1">; Assert | ||
failed: (< n 16)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
Using contract and with-constraints you were able to tighten the | ||
constraints on both the pre- and post-conditions of the sqr | ||
function. However, what if you wanted to relax the requirements? | ||
Stay tuned. | ||
[return to documentation] | ||
|
||
[defconstrainedfn]: ./defconstrainedfn | ||
[with-constraints]: ../with-constraints/ | ||
[return to documentation]: ../docs.html | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,99 @@ | ||
provide | ||
======= | ||
|
||
While defining contracts local to the constrained function is nice | ||
(see [defconstrainedfn] for more information), very often you will find | ||
yourself in possession of an existing function that is not | ||
constrained: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC3"><span class="p">(</span><span | ||
class="nf">sqr</span> <span class="mi">0</span><span | ||
class="p">)</span></div><div class="line" id="LC4"><span | ||
class="c1">;=> 0</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
In this case, core.contracts provides the provide-contracts macro to | ||
define contracts and apply them dynamically to existing functions: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="nf">provide-contracts</span> </div><div class="line" | ||
id="LC2"> <span class="p">[</span><span | ||
class="nv">sqr</span> <span class="s">"Constraints for | ||
squaring"</span> </div><div class="line" | ||
id="LC3"> <span class="p">[</span><span | ||
class="nv">x</span><span class="p">]</span> <span | ||
class="p">[</span><span class="nv">number?</span> <span | ||
class="p">(</span><span class="nb">not= </span><span | ||
class="mi">0</span> <span class="nv">x</span><span class="p">)</span> | ||
<span class="nv">=></span> <span class="nv">number?</span> <span | ||
class="nv">pos?</span><span class="p">]])</span></div><div | ||
class="line" id="LC4"><br/></div><div class="line" id="LC5"><span | ||
class="p">(</span><span class="nf">sqr</span> <span | ||
class="mi">0</span><span class="p">)</span></div><div class="line" | ||
id="LC6"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC7"><span class="c1">; Assert | ||
failed: (not= 0 n)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
As shown, the sqr function is dynamically modified with the contract | ||
defined in the body of provide-contracts. This macro can take any | ||
number of vectors where each corresponds to a contract for a given | ||
function; including multiple arities embedded within. core.contracts | ||
also allows you to include existing named contracts (see [defcontract] | ||
for more information) instead of the contract specification vector, as | ||
shown below: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="nf">defcontract</span> <span | ||
class="nv">sqr-contract</span></div><div class="line" | ||
id="LC2"> <span class="s">"Defines the constraints on | ||
squaring."</span></div><div class="line" id="LC3"> <span | ||
class="p">[</span><span class="nv">n</span><span class="p">]</span> | ||
<span class="p">[</span><span class="nv">number?</span> <span | ||
class="p">(</span><span class="nb">not= </span><span | ||
class="mi">0</span> <span class="nv">n</span><span class="p">)</span> | ||
<span class="nv">=></span> <span class="nv">pos?</span> <span | ||
class="nv">number?</span><span class="p">])</span></div><div | ||
class="line" id="LC4"><br/></div><div class="line" id="LC5"><span | ||
class="p">(</span><span class="nf">sqr</span> <span | ||
class="mi">0</span><span class="p">)</span></div><div class="line" | ||
id="LC6"><span class="c1">;=> 0</span></div><div class="line" | ||
id="LC7"><br/></div><div class="line" id="LC8"><span | ||
class="p">(</span><span class="nf">provide-contracts</span></div><div | ||
class="line" id="LC9"> <span class="p">[</span><span | ||
class="nv">sqr</span> <span class="s">"Apply the contract for | ||
squaring"</span> </div><div class="line" | ||
id="LC10"> <span | ||
class="nv">sqr-contract</span><span class="p">])</span></div><div | ||
class="line" id="LC11"><br/></div><div class="line" id="LC12"><span | ||
class="p">(</span><span class="nf">sqr</span> <span | ||
class="mi">0</span><span class="p">)</span></div><div class="line" | ||
id="LC13"><span class="c1">; java.lang.AssertionError: | ||
</span></div><div class="line" id="LC14"><span class="c1">; Assert | ||
failed: (not= 0 n)</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
provide-contracts gives you a lot of flexibilty in how to separate | ||
functions from their contracts and likewise apply them in | ||
domain-specific ways. | ||
[return to documentation] | ||
|
||
[defconstrainedfn]: ../defconstrainedfn/ | ||
[defcontract]: ./defcontract/ | ||
[return to documentation]: ../docs.html | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
references | ||
========== | ||
|
||
## 1) clojure.core.contracts references | ||
|
||
* [A Proof Engine for Eiffel]([http://tecomp.sourceforge.net/index.php?file=doc/papers/proof/engine]) | ||
* [An Axiomatic Basis for Computer Programming]([http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392]) by C.A.R Hoare -- essential reading | ||
* [Behavioral Software Contracts]([http://eecs.northwestern.edu/~robby/pubs/papers/behavioral-software-contracts.pdf]) (PDF) by Robert Bruce Findler | ||
* [Contract Programming in D]([http://www.digitalmars.com/d/2.0/dbc.html]) | ||
* [Contract Soundness for Object-Oriented Languages]([http://www.ccs.neu.edu/scheme/pubs/oopsla01-ff.pdf]) by Robert Bruce Findler and Matthias Felleisen | ||
* [Contracts for Higher-order functions]([http://www.ccs.neu.edu/racket/pubs/NU-CCIS-02-05.pdf]) by Robert Bruce Findler and Matthias Felleisen | ||
* [Contracts in Racket (A Scheme Descendent)]([http://pre.plt-scheme.org/docs/html/guide/contracts.html]) | ||
* [Design by Contract and Unit Testing]([http://onestepback.org/index.cgi/Tech/Programming/DbcAndTesting.html]) | ||
* [Design by contract for Ruby]([http://split-s.blogspot.com/2006/02/design-by-contract-for-ruby.html]) | ||
* [Eiffel: The Language]([http://www.amazon.com/dp/0132479257]) by Bertrand Meyer | ||
* [Fortress Language Specification]([http://labs.oracle.com/projects/plrg/fortress.pdf]) (PDF) by Guy L. Steele Jr., et al. | ||
* [How to Deign Programs]([http://htdp.org/]) by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi [here]([http://www.htdp.org/2003-09-26/Book/]) | ||
* [Jass - Java with Assertions]([http://www.eecs.northwestern.edu/~robby/contract-reading-list/jass.pdf]) (PDF) by Detlef Bartetzko, Clemens Fischer, Michael Moller and Heike Wehrheim | ||
* [Object-oriented Software Construction](ttp://www.amazon.com/dp/0136291554) by Bertrand Meyer | ||
* [System.Diagnostics.Contracts]([http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.aspx]) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
with-constraints | ||
================ | ||
|
||
core.contracts's with-constraints macro takes a function followed by | ||
one or more contracts and returns a new function that is the | ||
amalgamation of them all: | ||
<div class="gist"> | ||
<div class="gist-file"> | ||
<div class="gist-data gist-syntax"> | ||
<div class="gist-highlight"> | ||
<pre><div class="line" id="LC1"><span class="p">(</span><span | ||
class="k">def </span><span class="nv">constrained-sqr</span> | ||
</div><div class="line" id="LC2"> <span | ||
class="p">(</span><span class="nf">with-constraints</span></div><div | ||
class="line" id="LC3"> <span | ||
class="nv">sqr</span></div><div class="line" | ||
id="LC4"> <span | ||
class="nv">sqr-contract</span><span class="p">))</span></div></pre> | ||
</div> | ||
</div> | ||
</div> | ||
</div> | ||
See the docs of [contract] for more detail. | ||
[return to documentation] | ||
|
||
[contract]: ./contract/ | ||
[return to documentation]: ../docs.html | ||
|