@requires w = 5 && y = 7
@ensures  w*w + x = y*y + z
@program 
     @var w,x,y,z : int
     x = 6;
     z = 8;
     w = w*2 - 5;
     x = (x-1)*(x-1);
     y = y-2;
     z = (z+2)*(z+2);
     z = z-75;
@end
--
The lexical analyzer will not read past 
'--', so everything here is just a comment.