tp
Class PVis

java.lang.Object
  extended by tp.PVis
Direct Known Subclasses:
SVis

public class PVis
extends java.lang.Object


Nested Class Summary
Modifier and Type Class and Description
(package private) static interface PVis.Ap_package
          package nested annotation
protected static interface PVis.Ap_protected
          protected nested annotation
static interface PVis.Ap_public
          public nested annotation
(package private) static class PVis.Cp_package
           
protected static class PVis.Cp_protected
           
static class PVis.Cp_public
          private model constructor
(package private) static class PVis.EP_package
           
protected static class PVis.EP_protected
           
static class PVis.EP_public
           
(package private) static interface PVis.Ip_package
          package nested interface
protected static interface PVis.Ip_protected
          protected nested interface
static interface PVis.Ip_public
          public nested interface
 
JML Nested Model Class Summary
Modifier and Type Class and Description
@Model (package private) static interface tp.PVis.AMp_package
          package nested model annotation
@Model protected static interface tp.PVis.AMp_protected
          protected nested model annotation
@Model static interface tp.PVis.AMp_public
          public nested model annotation
@Model (package private) static class tp.PVis.Dp_package
           
@Model protected static class tp.PVis.Dp_protected
           
@Model static class tp.PVis.Dp_public
           
@Model (package private) static class tp.PVis.EMp_package
          package nested model enum
@Model protected static class tp.PVis.EMp_protected
          protected nested model enum
@Model static class tp.PVis.EMp_public
          public nested model enum
@Model (package private) static interface tp.PVis.IMp_package
          package nested model interface
@Model protected static interface tp.PVis.IMp_protected
          protected nested model interface
@Model static interface tp.PVis.IMp_public
          public nested model interface
 
Field Summary
Modifier and Type Field and Description
(package private)  int ip_package
           
protected  int ip_protected
           
 int ip_public
           
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Ghost (package private)  int gp_package
           
@Ghost protected  int gp_protected
           
@Ghost  int gp_public
           
 
Constructor Summary
Modifier Constructor and Description
  PVis()
          public constructor
protected PVis(int i)
          protected constructor
(package private) PVis(int i, int j)
          package constructor
 
JML Model Constructor Summary
Modifier Constructor and Description
protected PVis(float i)
          protected model constructor
(package private) PVis(float i, float j)
          package model constructor
  PVis(java.lang.Object o)
          public model constructor
 
Method Summary
Modifier and Type Method and Description
(package private)  void mp_package()
           
protected  void mp_protected()
           
 void mp_public()
           
 
JML Model Method Summary
Modifier and Type Method and Description
@Model (package private)  void qp_package()
           
@Model protected  void qp_protected()
           
@Model  void qp_public()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

ip_public

public int ip_public

ip_protected

protected int ip_protected

ip_package

int ip_package
JML Ghost Field Detail

gp_public

@Ghost
public int gp_public
 

JML Specifications: @Ghost



gp_protected

@Ghost
protected int gp_protected
 

JML Specifications: @Ghost



gp_package

@Ghost
int gp_package
 

JML Specifications: @Ghost


Constructor Detail

PVis

public PVis()
public constructor



PVis

protected PVis(int i)
protected constructor



PVis

PVis(int i,
     int j)
package constructor


JML Model Constructor Detail

PVis

@Model
public PVis(java.lang.Object o)
public model constructor


JML Constructor Specifications: @Model


PVis

@Model
protected PVis(float i)
protected model constructor


JML Constructor Specifications: @Model


PVis

@Model
PVis(float i,
           float j)
package model constructor


JML Constructor Specifications: @Model

Method Detail

mp_public

public void mp_public()


mp_protected

protected void mp_protected()


mp_package

void mp_package()

JML Model Method Detail

qp_public

@Model
public void qp_public()

JML Method Specifications: @Model


qp_protected

@Model
protected void qp_protected()

JML Method Specifications: @Model


qp_package

@Model
void qp_package()

JML Method Specifications: @Model