- Write down invariants for the window life cycle, especially:
    - When are borders set?  Prove that the current handling is sufficient.