Un exemple de vérification de programme : les N reines

Cette page présente la vérification formelle à l'aide des outils Why et Caduceus du programme C suivant : 
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));}
Ce programme est dû Marcel van Kervinck et a été trouvé sur cette page.
American