View source

[http://caduceus.lri.fr/ Caduceus] has been used to solve a simple "N-queens on a chessboard" problem.
[http://why.lri.fr/queens/index.en.html More information about the Queens problem with Caduceus is available on-line]; the [http://why.lri.fr/queens/slides-pp.pdf slides] are a good place to start and there is a [http://why.lri.fr/queens/queens.ps paper with more detail].

It's a tiny toy problem, but useful for teaching how to develop proofs. Jean-Christophe Filli&#226;tre notes that "in two lines of code we have C idiomatic bitwise operations, loops &amp; recursion involved in a backtracking algorithm, and highly efficient code".

This is an open proof because:
* The implementation is FLOSS, more specifically, the software being proved is in the public domain.  See below.
* The proof is FLOSS.  The proof is included in the Caduceus distribution, all of which was released under the GNU Public License (GPL) version 2.
* Required tools are FLOSS.  It can be modified with FLOSS text editors, the code can be compiled with a FLOSS C compiler (such as gcc), and the Caduceus tool (used for proof) is released under the GPL.  The tools necessary to support Caduceus (e.g., Why, alt-ergo, and Coq or PVS) are FLOSS as well.

This program was originally written in 2 obscure lines; it can be reformatted (and a minor ANSI C error fixed) into this more readable program:
<source lang="c">
 int t(int a, int b, int c) {
  int d, e=a&;~b&;~c, f=1;
  if (a)
   for (f=0; d=e&;-e; e-=d)
    f += t(a-d,(b+d)*2,(c+d)/2));
  return f;
 }
 int main(int n) {
  return t(~(~0<<n),0,0);
 }
</source>

This is a standalone
C program which reads an integer n on standard input and prints
the number of ways that n queens can be put
on a n × n chessboard so that they do not attack each other.
It requires that n be smaller than the machine word size in
bits (typically 32).

Unfortunately, the original release did not determine the license that covered the software being evaluated.  It is so short that it could be argued that copyright did not apply, but this is a shaky ground to stand on.  David A. Wheeler tracked down the original author, who graciously released this code to the public domain.  Here is his message (with some material modified to counter spam), showing that the original proved program is indeed FLOSS:

 From marcel k, (at) bitpit.net Mon Feb 25 10:36:15 2008
 Return-path: marcelk, (at) bitpit.net
 Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
 Message-Id: F185DFA6-8AF8-4612-8F1F-DE55AB749FC9, at, bitpit.net
 Content-Transfer-Encoding: 7bit
 From: Marcel van Kervinck marcelk, (at) bitpit.net
 Subject: Re: Would you release "queens" as Free Software / Open Source Software? (xyzzy)
 Date: Mon, 25 Feb 2008 17:36:00 +0800
 To: dwheeler, (at) dwheeler.com
 
 Hello David,
 
 I have no problem at all with your request.
 
 I posted the queens program over 13 years ago on usenet with no
 other thoughts than to share it openly without constraints (except
 maybe attribution).
 
 I think it is open by default in most countries by my posting
 and by it being so small, but in case there is any doubt, I
 hereby declare the program public domain explicitely:
 
 Version 1
 
 t(a,b,c){int d=0,e=a&amp;~b&amp;~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
 c+d)/2));return f;}main(q){scanf("%d",&amp;q);printf("%d\n",t(~(~0&lt;&lt;q),0,0));}
 
 This version unfortunately contains a bug that allows the compiler
 to give it a different interpretation than intended. I should have
 known better at the time when I posted it. Although it is wrong,
 it is the original form in which it was posted and it may have some
 odd kind of historical value for that reason.
 
 Today I prefer the following version of the queens program:
 
 Version 2
 
 t(a,b,c){int d=0,e=a&amp;~b&amp;~c,f=1;if(a)for(f=0;e-=d,d=e&-e;f+=t(a-d,(b+d)*2,(
 c+d)/2));return f;}main(q){scanf("%d",&amp;q);printf("%d\n",t(~(~0&lt;&lt;q),0,0));}
 
 Recently I found a rather trivial shorter version that also removes some
 unnecessary obfuscation. For completeness, here it is:
 
 Version 3
 
 t(a,b,c){int d=0,e=a&amp;~b&amp;~c,f=1;if(a)for(f=0;d=e&amp;-e;f+=t(a-d,(b+d)*2,(c+d)/
 2))e-=d;return f;}main(q){scanf("%d",&amp;q);printf("%d\n",t(~(~0&lt;&lt;q),0,0));}
 
 It is one character shorter and somewhat clearer, but it has lost
 some of its "charm" in the process...
 
 These other versions, as well as this e-mail, are also public domain
 of course.
 
 Kind regards,
 
 	Marcel van Kervinck
 
 On 20 Feb, 2008, at 23:23, David A. Wheeler wrote:
 
 > Hi  - I have a strange request.
 >
 > The following 2-liner has been attributed to you:
 > t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b 
 > +d)*2,(
 > c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q), 
 > 0,0));}
 >
 > If you're the author, would you please release this as open source  
 > software?
 > A simple declaration that "I release this under the GNU GPL version  
 > 2 or greater",
 > or some other license that you decide (such as LGPL, BSD-new, MIT),  
 > would be enough.
 > Or just declare that it's in the public domain, that'd be fine too.
 >
 > The reason is that I'm trying to encourage development of "open  
 > proofs" -
 > programs where EVERYTHING (programs, compilation tools, specs,  
 > proofs, and
 > proof tools) are Free-Libre / Open Source Software (FLOSS).  This  
 > would help.
 >
 > Thanks.
 >
 > --- David A. Wheeler
 >