javax.servlet.http
Interface HttpSession

public interface HttpSession

JML's specification of HttpSession.

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()
long	getCreationTime()
String	getId()
long	getLastAccessedTime()
int	getMaxInactiveInterval()
ServletContext	getServletContext()
HttpSessionContext	getSessionContext()           Deprecated.
Object	getValue(String name)           Deprecated.
String[]	getValueNames()           Deprecated.
void	invalidate()
boolean	isNew()
void	putValue(String name, Object value)           Deprecated.
void	removeAttribute(String name)
void	removeValue(String name)           Deprecated.
void	setAttribute(String name, Object value)
void	setMaxInactiveInterval(int interval)

 

Method Detail

getCreationTime

public long getCreationTime()

getId

public String getId()

getLastAccessedTime

public long getLastAccessedTime()

getServletContext

public ServletContext getServletContext()

setMaxInactiveInterval

public void setMaxInactiveInterval(int interval)

getMaxInactiveInterval

public int getMaxInactiveInterval()

getSessionContext

public HttpSessionContext getSessionContext()

Deprecated.  

getAttribute

public Object getAttribute(String name)

getValue

public Object getValue(String name)

Deprecated.  

getAttributeNames

public Enumeration getAttributeNames()

Specifications:

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

getValueNames

public String[] getValueNames()

Deprecated.  

setAttribute

public void setAttribute(String name,
                         Object value)

putValue

public void putValue(String name,
                     Object value)

Deprecated.  

removeAttribute

public void removeAttribute(String name)

removeValue

public void removeValue(String name)

Deprecated.  

invalidate

public void invalidate()

isNew

public boolean isNew()