HttpServletRequestWrapper (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

javax.servlet.http
Class HttpServletRequestWrapper

java.lang.Object
  javax.servlet.ServletRequestWrapper
      javax.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