| method | com.dmdirc.addons.ui_swing.components. EtchedLineBorder$BorderSide__static_init |
| post | $VALUES == &new EtchedLineBorder$BorderSide[](E tchedLineBorder$BorderSide__static_init#3) |
| post | BOTTOM == &new EtchedLineBorder$BorderSide(Etch edLineBorder$BorderSide__static_init#2) |
| post | $VALUES[1] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#2) |
| post | TOP == &new EtchedLineBorder$BorderSide(EtchedL ineBorder$BorderSide__static_init#1) |
| post | $VALUES[0] == &new EtchedLineBorder$BorderSide( EtchedLineBorder$BorderSide__static_init#1) |
| post | new EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#1) num objects == 1 |
| post | new EtchedLineBorder$BorderSide(EtchedLineBorder$Bo rderSide__static_init#2) num objects == 1 |
| post | new EtchedLineBorder$BorderSide[](EtchedLineBorder$ BorderSide__static_init#3) num objects == 1 |
| post | $VALUES.length == 2 |
| unanalyzed | call on java.lang.Enum |
| method | void paintBorder(Component, Graphics, int, int, int, int) |
| pre | g != null |
| pre | init'ed(this.etchType) |
| pre | this.side != null |
| pre | x <= 231 |
| pre | y <= 231 |
| pre | (soft) init'ed(com.dmdirc.addons.ui_swing. components.EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...]) |
| pre | (soft) height >= -231+1 |
| pre | (soft) width >= -231+2 |
| presumption | com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@70 in {0,1} |
| presumption | com.dmdirc.addons.ui_swing.components. EtchedLineBorder_BorderSide:ordinal(...)@82 in {0,1} |
| test_vector | com.dmdirc.addons.ui_swing.components. EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...]: {1}, {2}, {-231..0, 3..232-1} |
| test_vector | this.etchType: {-231..0, 2.. 232-1}, {1} |