ServletOutputStream (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
Class ServletOutputStream

java.lang.Object
  java.io.OutputStream
      javax.servlet.ServletOutputStream

public abstract class ServletOutputStream
extends OutputStream

JML's specification of ServletOutputStream

Class Specifications

Specifications inherited from class OutputStream

public invariant ( \forall int i; 0 <= i&&i < this.outputBytes.size(); this.outputBytes.get(i) instanceof org.jmlspecs.models.JMLByte);
public invariant this.isOpen ==> !this.wasClosed;
public invariant this.wasClosed ==> !this.isOpen;
public constraint \old(this.wasClosed) ==> this.wasClosed;

Specifications inherited from class Object

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

Model Field Summary

Model fields inherited from class java.io.OutputStream

isOpen, output, outputBytes, wasClosed

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

Ghost Field Summary

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

Constructor Summary

protected ServletOutputStream()


Model Method Summary

Model methods inherited from class java.lang.Object

hashValue

Method Summary

void print(boolean b)


void print(char c)


void print(double d)


void print(float f)


void print(int i)


void print(String s)


void print(long l)


void println()


void println(boolean b)


void println(char c)


void println(double d)


void println(float f)


void println(int i)


void println(String s)


void println(long l)


Methods inherited from class java.io.OutputStream

close, flush, write, write, write

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail