// ----------------------------------------------------------------- // chess.txt: n queens and knight's tour // Concrete Abstractions: Puzzles and Games // (c) 2020, Wolfgang Schreiner, RISC, JKU Linz, Austria // ----------------------------------------------------------------- // board size val N:ℕ; axiom notNull ⇔ N > 0; // true if all solutions are to be printed (just one, otherwise) val printall = true; // ----------------------------------------------------------------- // N queens // ----------------------------------------------------------------- type Num = ℕ[N]; type Queens = Array[N,Num]; pred admissible(q:Queens,n:Num,p:Num) ⇔ n < N ∧ p < N ∧ ∀i:Num with i < n. q[i] ≠ p ∧ q[i]-i ≠ p-n ∧ q[i]+i ≠ p+n; shared system Queens { var q:Queens = Array[N,Num](N); var n:Num = 0; invariant n < N; // invariant n = N ⇒ print q in ⊤; // invariant n = N ⇒ print q in printall; invariant n = N ⇒ printtrace in printall; action place(p:Num) with admissible(q,n,p); { q[n] ≔ p; n ≔ n+1; } } shared system Queens0 { var q:Queens; var n:Num; invariant n < N; init() ⇔ q0 = Array[N,Num](N) ∧ n0 = 0; action place(p:Num) ⇔ admissible(q,n,p) ∧ q0[n] = p ∧ (∀i:Num with i < n. q0[i] = q[i]) ∧ n0 = n+1; } // ----------------------------------------------------------------- // Knight's Tour // ----------------------------------------------------------------- // board positions and sequences of such positions val L = N⋅N; type Len = ℕ[L]; type Pos = Record[x:Num,y:Num]; type Positions = Array[L,Pos]; // jumps and the resulting offsets val J = 8; type Jump = ℕ[J-1]; type Offset = ℤ[-2,2]; val x = Array[J,Offset](-2,-2,-1,-1,1,1,2,2); val y = Array[J,Offset](-1,1,-2,2,-2,2,-1,1); pred admissible(pos:Positions,len:Len,j:Jump) ⇔ len < L ∧ let p = ⟨x:pos[len-1].x+x[j],y:pos[len-1].y+y[j]⟩ in 0 ≤ p.x ∧ p.x < N ∧ 0 ≤ p.y ∧ p.y < N ∧ ∀i:Len with i < len. pos[i] ≠ p; shared system Knight { var pos:Positions = Array[L,Pos](⟨x:N,y:N⟩); var len:Len = 1; invariant len = L ⇒ print pos in printall; init(p:Pos) with p.x < N ∧ p.y < N; { pos[0] := p; } action jump(j:Jump) with admissible(pos,len,j); { pos[len] ≔ ⟨x:pos[len-1].x+x[j],y:pos[len-1].y+y[j]⟩; len ≔ len+1; } } // ----------------------------------------------------------------- // end of file // -----------------------------------------------------------------