// ************************************************************************** // // eses eses // eses eses // eses eseses esesese eses Embedded Systems Group // ese ese ese ese ese // ese eseseses eseseses ese Department of Computer Science // eses eses ese eses // eses eseses eseseses eses University of Kaiserslautern // eses eses // // ************************************************************************** // // This Quartz program considers magic squares of size sizexsize(). In such a // square, the numbers 1,...,9 should be placed such that the sums of // all rows and columns is the same. // // It is well known that (up to permutations) there is only one // solution for the 3x3 square: // // ------------- // | 4 | 8 | 3 | // ------------- // | 2 | 6 | 7 | // ------------- // | 9 | 1 | 5 | // ------------- // // Clearly, the sum 15 is the only possibility, since the sum of all // numbers is 1+2+...+9 = 45 that will be partitioned into equally // sized parts for the three rows or the three columns. // // ************************************************************************** import MagicSquare.*; package MagicSquare; macro size = 3; module MagicSquare( [size][size()]nat{size()*size()} a, event !wrong_sum, no_perm ) { for(i=0..(size-1)) CheckRowSum (a,i,wrong_sum); for(i=0..(size-1)) CheckColSum (a,i,wrong_sum); for(i=0..(size-1)) CheckRowPerm(a,i,no_perm); for(i=0..(size-1)) CheckColPerm(a,i,no_perm); } satisfies { notmagic [DisProveA]: assert wrong_sum | no_perm; }