org.jmlspecs.jmlunit
Class FancyTabbedPrintWriter

java.lang.Object
  org.jmlspecs.jmlunit.FancyTabbedPrintWriter

public class FancyTabbedPrintWriter

extends Object

A more convenient print writer.

Version:

$Revision: 1.1 $

Author:

Gary T. Leavens

Class Specifications

public invariant this.TAB_SIZE > 0; public invariant 0 <= this.leftMargin; private invariant_redundantly this.tabSize > 0; private invariant this.pos >= 0; private represents TAB_SIZE <- this.tabSize; private represents leftMargin <- this.pos;

Specifications inherited from class Object

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

Model Field Summary
int	leftMargin
int	TAB_SIZE

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
private  int	pos
private  int	tabSize
private  TabbedPrintWriter	writer           The writer to which the output is to be printed.

 

Constructor Summary

FancyTabbedPrintWriter(non_null Writer writer)           Initialize this fancy tabbed print writer.

FancyTabbedPrintWriter(non_null Writer writer, int tabSize)           Initialize this fancy tabbed print writer.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	close()           Close this file.
void	indent()           Indents one TAB_SIZE.
void	newLine()           Prints a line separator.
void	print(Object s)           Prints the given object.
void	print(String s)           Prints the given string.
void	println(Object s)           Prints the given object with a trailing line separator.
void	printlnIn(Object s)           Prints the given object with one tabSize indentation and a trailing line separator.
void	setTabSize(int n)           Set the tab size to the given integer.
void	undent()           Und-ndents one tabSize.

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

TAB_SIZE

public int TAB_SIZE

Specifications:
datagroup contains: tabSize

leftMargin

public int leftMargin

Specifications:
datagroup contains: pos

writer

private TabbedPrintWriter writer

The writer to which the output is to be printed.

Specifications: non_null
is in groups: objectState
maps writer.objectState \into objectState

tabSize

private int tabSize

Specifications:
is in groups: TAB_SIZE

pos

private int pos

Specifications:
is in groups: leftMargin

FancyTabbedPrintWriter

public FancyTabbedPrintWriter(non_null Writer writer)

Initialize this fancy tabbed print writer. The default tab size, 4, is appropriate for emacs. (:-)

Specifications:

assignable objectState, TAB_SIZE, leftMargin;
ensures this.TAB_SIZE == 4&&this.leftMargin == 0;

FancyTabbedPrintWriter

public FancyTabbedPrintWriter(non_null Writer writer,
                              int tabSize)

Initialize this fancy tabbed print writer.

Specifications:

requires tabSize > 0;
assignable objectState, TAB_SIZE, leftMargin;
ensures this.TAB_SIZE == tabSize&&this.leftMargin == 0;

indent

public void indent()

Indents one TAB_SIZE.

Specifications:

requires this.leftMargin < 2147483647-this.TAB_SIZE;
assignable leftMargin;
ensures this.leftMargin == \old(this.leftMargin+this.TAB_SIZE);

undent

public void undent()

Und-ndents one tabSize.

Specifications:

requires 0 <= this.leftMargin;
assignable leftMargin;
ensures this.leftMargin == \old(this.leftMargin-this.TAB_SIZE);

print

public void print(Object s)

Prints the given object.

Specifications:

assignable objectState;

print

public void print(String s)

Prints the given string.

Specifications:

assignable objectState;

println

public void println(Object s)

Prints the given object with a trailing line separator.

Specifications:

assignable objectState;

printlnIn

public void printlnIn(Object s)

Prints the given object with one tabSize indentation and a trailing line separator.

Specifications:

assignable objectState, leftMargin;
ensures \not_modified(leftMargin);

newLine

public void newLine()

Prints a line separator.

Specifications:

assignable objectState;

setTabSize

public void setTabSize(int n)

Set the tab size to the given integer.

Specifications:

requires n > 0;
assignable TAB_SIZE;
ensures this.TAB_SIZE == n;

close

public void close()

Close this file.

Specifications:

assignable objectState;