class interface
WIN_EVENT
invariant
good_window: window /= Void;
end of
WIN_EVENT