JML

javax.servlet.http
Class HttpServletRequestWrapper

java.lang.Object
  extended byjavax.servlet.ServletRequestWrapper
      extended byjavax.servlet.http.HttpServletRequestWrapper
All Implemented Interfaces:
HttpServletRequest, ServletRequest

public class HttpServletRequestWrapper
extends ServletRequestWrapper
implements HttpServletRequest

JML's specification of HttpServletRequestWrapper.


Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface HttpServletRequest
initially javax.servlet.http.HttpServletRequest.BASIC_AUTH == "BASIC";
initially javax.servlet.http.HttpServletRequest.FORM_AUTH == "FORM";
initially javax.servlet.http.HttpServletRequest.CLIENT_CERT_AUTH == "CLIENT_CERT";
initially javax.servlet.http.HttpServletRequest.DIGEST_AUTH == "DIGEST";

Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
 
Fields inherited from interface javax.servlet.http.HttpServletRequest
BASIC_AUTH, CLIENT_CERT_AUTH, DIGEST_AUTH, FORM_AUTH
 
Constructor Summary
HttpServletRequestWrapper(HttpServletRequest request)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 String getAuthType()
           
 String getContextPath()
           
 Cookie[] getCookies()
           
 long getDateHeader(String name)
           
 String getHeader(String name)
           
 Enumeration getHeaderNames()
           
 Enumeration getHeaders(String name)
           
 int getIntHeader(String name)
           
 String getMethod()
           
 String getPathInfo()
           
 String getPathTranslated()
           
 String getQueryString()
           
 String getRemoteUser()
           
 String getRequestedSessionId()
           
 String getRequestURI()
           
 StringBuffer getRequestURL()
           
 String getServletPath()
           
 HttpSession getSession()
           
 HttpSession getSession(boolean create)
           
 Principal getUserPrincipal()
           
 boolean isRequestedSessionIdFromCookie()
           
 boolean isRequestedSessionIdFromURL()
           
 boolean isRequestedSessionIdFromUrl()
           
 boolean isRequestedSessionIdValid()
           
 boolean isUserInRole(String role)
           
 
Methods inherited from class javax.servlet.ServletRequestWrapper
getAttribute, getAttributeNames, getCharacterEncoding, getContentLength, getContentType, getInputStream, getLocalAddr, getLocale, getLocales, getLocalName, getLocalPort, getParameter, getParameterMap, getParameterNames, getParameterValues, getProtocol, getReader, getRealPath, getRemoteAddr, getRemoteHost, getRemotePort, getRequest, getRequestDispatcher, getScheme, getServerName, getServerPort, isSecure, removeAttribute, setAttribute, setCharacterEncoding, setRequest
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface javax.servlet.ServletRequest
getAttribute, getAttributeNames, getCharacterEncoding, getContentLength, getContentType, getInputStream, getLocalAddr, getLocale, getLocales, getLocalName, getLocalPort, getParameter, getParameterMap, getParameterNames, getParameterValues, getProtocol, getReader, getRealPath, getRemoteAddr, getRemoteHost, getRemotePort, getRequestDispatcher, getScheme, getServerName, getServerPort, isSecure, removeAttribute, setAttribute, setCharacterEncoding
 

Constructor Detail

HttpServletRequestWrapper

public HttpServletRequestWrapper(HttpServletRequest request)
Method Detail

getAuthType

public String getAuthType()
Specified by:
getAuthType in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getCookies

public Cookie[] getCookies()
Specified by:
getCookies in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getDateHeader

public long getDateHeader(String name)
Specified by:
getDateHeader in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getHeader

public String getHeader(String name)
Specified by:
getHeader in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getHeaders

public Enumeration getHeaders(String name)
Specified by:
getHeaders in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getHeaderNames

public Enumeration getHeaderNames()
Specified by:
getHeaderNames in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getIntHeader

public int getIntHeader(String name)
Specified by:
getIntHeader in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getMethod

public String getMethod()
Specified by:
getMethod in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getPathInfo

public String getPathInfo()
Specified by:
getPathInfo in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getPathTranslated

public String getPathTranslated()
Specified by:
getPathTranslated in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getContextPath

public String getContextPath()
Specified by:
getContextPath in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getQueryString

public String getQueryString()
Specified by:
getQueryString in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getRemoteUser

public String getRemoteUser()
Specified by:
getRemoteUser in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

isUserInRole

public boolean isUserInRole(String role)
Specified by:
isUserInRole in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getUserPrincipal

public Principal getUserPrincipal()
Specified by:
getUserPrincipal in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getRequestedSessionId

public String getRequestedSessionId()
Specified by:
getRequestedSessionId in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getRequestURI

public String getRequestURI()
Specified by:
getRequestURI in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getRequestURL

public StringBuffer getRequestURL()
Specified by:
getRequestURL in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getServletPath

public String getServletPath()
Specified by:
getServletPath in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
ensures \result != null;

getSession

public HttpSession getSession(boolean create)
Specified by:
getSession in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

getSession

public HttpSession getSession()
Specified by:
getSession in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
ensures \result != null;

isRequestedSessionIdValid

public boolean isRequestedSessionIdValid()
Specified by:
isRequestedSessionIdValid in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

isRequestedSessionIdFromCookie

public boolean isRequestedSessionIdFromCookie()
Specified by:
isRequestedSessionIdFromCookie in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

isRequestedSessionIdFromURL

public boolean isRequestedSessionIdFromURL()
Specified by:
isRequestedSessionIdFromURL in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

isRequestedSessionIdFromUrl

public boolean isRequestedSessionIdFromUrl()
Specified by:
isRequestedSessionIdFromUrl in interface HttpServletRequest
Specifications inherited from overridden method in interface HttpServletRequest:
      --- None ---

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.