}
assert_all(bRulerEndpoints && nMarks==nM && bDistanceDiff);
The above specification employs a binary representation of the ruler (nRuler**) where**
each bit set denotes a mark. The value nRuler & nRuler >> nL & 1 equals 1 **if and only** if the first and nL**th bit are set (as the ruler endpoints). The value** nMarks **counts the bits** set (e.g., the marks) and it should equal nM**. If the ruler** nRuler **is a Golomb ruler, then** whenever it is shifted left (for values 1, **. . .**, nL-1**) and bitwise conjunction is performed with**
the original ruler giving the value n, there will be at most one bit set in n **(since all the**
differences between the marks are distinct). There is at most one bit set in n **if and only** if the value n & (n-1) **equals 0. This specification, employing a single loop, illustrate the**
expressive power of bitwise operations supported in the ursa **language.**
For the magic square problem, ursa **was used with the following specification:**
nDim=4; nN=nDim*nDim; bCorrectSum = (2*nSum*nDim == nN*(nN-1));
bDomain=true; bDistinct=true; for(ni=0;ni<nDim;ni++) {
for(nj=0;nj<nDim;nj++) {
bDomain &&= (nT[ni][nj]<nN);
for(nk=0;nk<nDim;nk++)
for(nl=0;nl<nDim;nl++)
bDistinct &&= ((ni==nk && nj==nl) || nT[ni][nj]!=nT[nk][nl]);
}
}
bSum=true; nSum1=0; nSum2=0; for(ni=0;ni<nDim;ni++) {
nSum1 += nT[ni][ni];
nSum2 += nT[ni][nDim-ni-1]; nSum3=0; nSum4=0; for(nj=0;nj<nDim;nj++) {
nSum3 += nT[ni][nj];
nSum4 += nT[nj][ni];
} bSum &&= (nSum3==nSum);
bSum &&= (nSum4==nSum);
} bSum &&= (nSum1==nSum);
bSum &&= (nSum2==nSum);
assert_all(bCorrectSum && bDomain && bDistinct && bSum);
For the linear recursive relation, ursa **was used with the following specification (the**
specification for the non-recursive relations is analogous):
n = 30; ny = 20603361;