JML

javax.servlet.http
Interface HttpServletRequest

All Superinterfaces:
ServletRequest
All Known Implementing Classes:
HttpServletRequestWrapper

public interface HttpServletRequest
extends ServletRequest

JML's specification of HttpServletRequest.


Class Specifications
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";

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

Field Summary
static String BASIC_AUTH
           
static String CLIENT_CERT_AUTH
           
static String DIGEST_AUTH
           
static String FORM_AUTH
           
 
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()
          Deprecated.  
 boolean isRequestedSessionIdValid()
           
 boolean isUserInRole(String role)
           
 
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
 

Field Detail

BASIC_AUTH

public static final String BASIC_AUTH

FORM_AUTH

public static final String FORM_AUTH

CLIENT_CERT_AUTH

public static final String CLIENT_CERT_AUTH

DIGEST_AUTH

public static final String DIGEST_AUTH
Method Detail

getAuthType

public String getAuthType()

getCookies

public Cookie[] getCookies()

getDateHeader

public long getDateHeader(String name)

getHeader

public String getHeader(String name)

getHeaders

public Enumeration getHeaders(String name)

getHeaderNames

public Enumeration getHeaderNames()

getIntHeader

public int getIntHeader(String name)

getMethod

public String getMethod()

getPathInfo

public String getPathInfo()

getPathTranslated

public String getPathTranslated()

getContextPath

public String getContextPath()

getQueryString

public String getQueryString()

getRemoteUser

public String getRemoteUser()

isUserInRole

public boolean isUserInRole(String role)

getUserPrincipal

public Principal getUserPrincipal()

getRequestedSessionId

public String getRequestedSessionId()

getRequestURI

public String getRequestURI()

getRequestURL

public StringBuffer getRequestURL()

getServletPath

public String getServletPath()
Specifications:
ensures \result != null;

getSession

public HttpSession getSession(boolean create)

getSession

public HttpSession getSession()
Specifications:
ensures \result != null;

isRequestedSessionIdValid

public boolean isRequestedSessionIdValid()

isRequestedSessionIdFromCookie

public boolean isRequestedSessionIdFromCookie()

isRequestedSessionIdFromURL

public boolean isRequestedSessionIdFromURL()

isRequestedSessionIdFromUrl

public boolean isRequestedSessionIdFromUrl()
Deprecated.  


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.