JML

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()

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.