tp
Class PVis

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

public class PVis
extends java.lang.Object


Nested Class Summary
Modifier and Type Class and Description
static interface PVis.Ap_public
          public nested annotation
static class PVis.Cp_public
          private model constructor
static class PVis.EP_public
           
static interface PVis.Ip_public
          public nested interface
 
JML Nested Model Class Summary
Modifier and Type Class and Description
@Model static interface tp.PVis.AMp_public
          public nested model annotation
@Model static class tp.PVis.Dp_public
           
@Model static class tp.PVis.EMp_public
          public nested model enum
@Model static interface tp.PVis.IMp_public
          public nested model interface
 
Field Summary
Modifier and Type Field and Description
 int ip_public
           
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Ghost  int gp_public
           
 
Constructor Summary
Constructor and Description
PVis()
          public constructor
 
JML Model Constructor Summary
Constructor and Description
PVis(java.lang.Object o)
          public model constructor
 
Method Summary
Modifier and Type Method and Description
 void mp_public()
           
 
JML Model Method Summary
Modifier and Type Method and Description
@Model  void qp_public()
           
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

ip_public

public int ip_public
JML Ghost Field Detail

gp_public

@Ghost
public int gp_public
 

JML Specifications: @Ghost


Constructor Detail

PVis

public PVis()
public constructor


JML Model Constructor Detail

PVis

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


JML Constructor Specifications: @Model

Method Detail

mp_public

public void mp_public()

JML Model Method Detail

qp_public

@Model
public void qp_public()

JML Method Specifications: @Model