class Global ^=
abstract
   var inLine: map of ( (set of Posn) -> bool );
   
   invariant (forall ps::set of Posn :- (inLine[ps] <==> 
   		((exists s:: set of set of nat{
   				   set of nat{0,1,2}, set of nat{3,4,5}, set of nat {6,7,8},
   				   set of nat{0,3,6}, set of nat{1,4,7}, set of nat {2,5,8},
   				   set of nat{0,4,8}, set of nat{2,4,6}} :- (s <<= ps)))));
interface
    build{!inLine:map of ( (set of Posn) -> bool )}
    	pre (forall ps::set of Posn :- (inLine[ps] <==> 
   				((exists s:: set of set of nat{
   				   set of nat{0,1,2}, set of nat{3,4,5}, set of nat {6,7,8},
   				   set of nat{0,3,6}, set of nat{1,4,7}, set of nat {2,5,8},
   				   set of nat{0,4,8}, set of nat{2,4,6}} :- (s <<= ps))))) 
    ;
    
    function inLine;
end;