| post | init'ed(new ValidationResponse(validate#2*). failure) |
| post | new ValidationResponse(validate#1*) num objects <= 1 |
| post | new ValidationResponse(validate#1*).failure == null |
| post | new ValidationResponse(validate#2*) num objects <= 1 |
| post | new ValidationResponse(validate#2*).failure == this.failedReason |
| post | return_value == One-of{&new ValidationResponse( validate#1*), &new ValidationResponse(validate# 2*)} |
| post | return_value in Addr_Set{&new ValidationRespons e(validate#1*),&new ValidationResponse(validate #2*)} |