javax.servlet
Interface ServletRequest

All Known Subinterfaces:

HttpServletRequest

All Known Implementing Classes:

HttpServletRequestWrapper, ServletRequestWrapper

public interface ServletRequest

JML's specification of ServletRequest

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Method Summary
Object	getAttribute(String name)
Enumeration	getAttributeNames()
String	getCharacterEncoding()
int	getContentLength()
String	getContentType()
ServletInputStream	getInputStream()
String	getLocalAddr()
Locale	getLocale()
Enumeration	getLocales()
String	getLocalName()
int	getLocalPort()
String	getParameter(String name)
Map	getParameterMap()
Enumeration	getParameterNames()
String[]	getParameterValues(String name)
String	getProtocol()
BufferedReader	getReader()
String	getRealPath(String path)           Deprecated.
String	getRemoteAddr()
String	getRemoteHost()
int	getRemotePort()
RequestDispatcher	getRequestDispatcher(String path)
String	getScheme()
String	getServerName()
int	getServerPort()
boolean	isSecure()
void	removeAttribute(String name)
void	setAttribute(String name, Object o)
void	setCharacterEncoding(String env)

 

Method Detail

getAttribute

public Object getAttribute(String name)

getAttributeNames

public Enumeration getAttributeNames()

Specifications:

ensures \result != null&&\result .elementType == java.lang.String.class;

getCharacterEncoding

public String getCharacterEncoding()

setCharacterEncoding

public void setCharacterEncoding(String env)
                                   throws UnsupportedEncodingException

Throws:

UnsupportedEncodingException

getContentLength

public int getContentLength()

getContentType

public String getContentType()

getInputStream

public ServletInputStream getInputStream()
                                           throws IOException

Throws:

IOException

getParameter

public String getParameter(String name)

Specifications:

assignable \nothing;

getParameterNames

public Enumeration getParameterNames()

Specifications:

ensures \result != null&&\result .elementType == java.lang.String.class;

getParameterValues

public String[] getParameterValues(String name)

getParameterMap

public Map getParameterMap()

getProtocol

public String getProtocol()

getScheme

public String getScheme()

getServerName

public String getServerName()

getServerPort

public int getServerPort()

getReader

public BufferedReader getReader()
                                  throws IOException

Throws:

IOException

getRemoteAddr

public String getRemoteAddr()

getRemoteHost

public String getRemoteHost()

setAttribute

public void setAttribute(String name,
                         Object o)

Specifications:

public behavior
assignable objectState;

removeAttribute

public void removeAttribute(String name)

getLocale

public Locale getLocale()

getLocales

public Enumeration getLocales()

isSecure

public boolean isSecure()

getRequestDispatcher

public RequestDispatcher getRequestDispatcher(String path)

getRealPath

public String getRealPath(String path)

Deprecated.  

getRemotePort

public int getRemotePort()

getLocalName

public String getLocalName()

getLocalAddr

public String getLocalAddr()

getLocalPort

public int getLocalPort()