PreviousCommand.java |
| current inspection = 2009-09-03 21:56:13 (id #1) |
|
|
| Kind | Annotation Text |
|---|---|
| post | init'ed(this.line) |
| post | init'ed(this.time) |
| post | this.line == line |
| Kind | Annotation Text |
|---|
| Kind | Annotation Text |
|---|---|
| post | init'ed(return_value) |
| test_vector | java.lang. |
| test_vector | obj: Inverse{null}, |
| test_vector | this.line == obj. |
| test_vector | this.line: |
| Kind | Annotation Text |
|---|---|
| post | init'ed(return_value) |
| post | return_value == this.line |
| Kind | Annotation Text |
|---|---|
| post | init'ed(return_value) |
| post | return_value == this.time |
| Kind | Annotation Text |
|---|---|
| presumption | java.lang. |
| post | return_value >= -2_ |