AppUrl.java |
| current inspection = 2009-09-04 18:33:31 (id #2) | base = 2009-09-04 18:33:31 (id #1) |
|
|
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | init'ed(this. | 2009-09-04 18:33:31 |
| + | post | init'ed(return_value) | 2009-09-04 18:33:31 |
| + | post | return_value == this. | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | init'ed(this.handle) | 2009-09-04 18:33:31 |
| + | post | init'ed(return_value) | 2009-09-04 18:33:31 |
| + | post | return_value == this.handle | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | init'ed(this. | 2009-09-04 18:33:31 |
| + | post | init'ed(return_value) | 2009-09-04 18:33:31 |
| + | post | return_value == this. | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | post | new URL(AppUrl#1) num objects == 1 | 2009-09-04 18:33:31 |
| + | post | new URL(AppUrl#3) num objects == 1 | 2009-09-04 18:33:31 |
| + | post | this.entryUrl == &new URL( | 2009-09-04 18:33:31 |
| + | post | this.resourceUrl == &new URL( | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | ENDPOINT_ | 2009-09-04 18:33:31 |
| + | pre | ID_PATTERN != null | 2009-09-04 18:33:31 |
| + | pre | url != null | 2009-09-04 18:33:31 |
| + | post | init'ed(this.handle) | 2009-09-04 18:33:31 |
| + | post | new URL(AppUrl#1) num objects == 1 | 2009-09-04 18:33:31 |
| + | post | new URL(AppUrl#3) num objects == 1 | 2009-09-04 18:33:31 |
| + | post | this.entryUrl == &new URL( | 2009-09-04 18:33:31 |
| + | post | this.resourceUrl == &new URL( | 2009-09-04 18:33:31 |
| + | unanalyzed | call on java.net.URL | 2009-09-04 18:33:31 |
| + | unanalyzed | call on java. | 2009-09-04 18:33:31 |
| + | unanalyzed | call on java. | 2009-09-04 18:33:31 |
| + | unanalyzed | call on java. | 2009-09-04 18:33:31 |
| + | unanalyzed | call on java. | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | post | init'ed(ENDPOINT_ | 2009-09-04 18:33:31 |
| + | post | init'ed(ID_ | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | ENDPOINT_ | 2009-09-04 18:33:31 |
| + | pre | url != null | 2009-09-04 18:33:31 |
| + | presumption | java.util. | 2009-09-04 18:33:31 |
| + | post | new URL(parseEndpoint#1) num objects <= 1 | 2009-09-04 18:33:31 |
| + | post | return_value == One-of{null, | 2009-09-04 18:33:31 |
| + | post | return_value in Addr_ | 2009-09-04 18:33:31 |
| + | test_vector | java.util. | 2009-09-04 18:33:31 |
| -/+ | Kind | Annotation Text | Date |
|---|---|---|---|
| + | pre | ID_PATTERN != null | 2009-09-04 18:33:31 |
| + | pre | url != null | 2009-09-04 18:33:31 |
| + | presumption | java.util. | 2009-09-04 18:33:31 |
| + | post | init'ed(return_value) | 2009-09-04 18:33:31 |
| + | test_vector | java.util. | 2009-09-04 18:33:31 |