| method | View process(HttpServletRequest, HttpServletRespon se) |
| pre | request != null |
| pre | response != null |
| presumption | javax.servlet.http.HttpServletRequest:getSession(.. .)@59 != null |
| post | return_value == &new RedirectView(process#2) |
| post | new RedirectView(process#2) num objects == 1 |