@requires x = m && y = n

@ensures  x = n && y = m

@program  
     @var x, y, m, n : int
      x = x + y;  
      y = x - y; 			 
      x = x - y;
@end
--
The lexical analyzer will not read past
the two dashes, so everything here is just a comment.