| method | com.dmdirc.installer.ui.EtchedLineBorder$BorderSid e__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.installer.ui. EtchedLineBorder$1__static_init.new int[](EtchedLineBorder$1__static_init#1)[...]) |
| pre | (soft) height <= 232-6 |
| pre | (soft) width <= 232-6 |
| presumption | com.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@75 in {0,1} |
| presumption | com.dmdirc.installer.ui.EtchedLineBorder_ BorderSide:ordinal(...)@88 in {0,1} |
| test_vector | com.dmdirc.installer.ui.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} |