Author: James Murphy
Date: 07:47:09 04/20/04
Hi, I have written a two player chess program in Java and I am in the process of evaluating it i.e. performing tests and measures on how well it accomplishes its objectives. Since one of the objectives of the program is to play chess, an obvious evaluation would be to porve that the program actually does play chess. To do this, I would have to establish some correctness properties of a chess-playing program (for a particular input, a certain output is exptected) and prove that my program holds true for them. I believe the correctness properties of a chess-playing program are: 1) Pieces can only move and capture in certain ways; illegal moves are not permissible 2) Check requires a player to move out of check 3) Game terminations (checkmate/stalemate) should be correctly detected Can anyone suggest anymore if there are any? There are two ways to prove a chess program is correct; testing and formal proofs. Full testing is impractical as not every input can be tested against every output because it would take too long (10^38 seconds I think. Not sure if thats right). Therefore equivalance testing is used where we say that if a piece passes a move test, it will pass for a similar range of values on the chess board. If it fails, it will also fail for a range of values on the chessboard. This will therefore prove that the program is correct. To increase our confidence in these test, formal proofs could also be used. A formal proof requires a little more work to construct however. Does anyone have any advice on how to construct a formal proof for a chess program. I have some idea but I'm not totally clear where to start on it. I guess I must have to reason about the code or something using induction perhaps. All help appreciated. Also if any of my reasoning above is incorrect I would also appreciate your corrections/additions. Thanks
This page took 0 seconds to execute
Last modified: Thu, 15 Apr 21 08:11:13 -0700
Current Computer Chess Club Forums at Talkchess. This site by Sean Mintz.