Class Vis

java.lang.Object
  extended by tp.PVis
      extended by Vis

public class Vis
extends PVis


Nested Class Summary
Modifier and Type Class and Description
protected static interface SVis.As_protected
          protected nested annotation
static interface SVis.As_public
          public nested annotation
protected static class SVis.Cs_protected
           
static class SVis.Cs_public
          private model constructor
protected static class SVis.ES_protected
           
static class SVis.ES_public
           
protected static interface SVis.Is_protected
          protected nested interface
static interface SVis.Is_public
          public nested interface
protected static interface Vis.A_protected
          protected nested annotation
static interface Vis.A_public
          public nested annotation
protected static class Vis.C_protected
          protected nested class
static class Vis.C_public
          public nested class
protected static class Vis.E_protected
          protected nested enum
static class Vis.E_public
          public nested enum
protected static interface Vis.I_protected
          protected nested interface
static interface Vis.I_public
          public nested interface
 
JML Nested Model Class Summary
Modifier and Type Class and Description
@Model protected static interface Vis.AM_protected
          protected nested model annotation
@Model static interface Vis.AM_public
          public nested model annotation
@Model protected static class Vis.D_protected
          protected nested model class
@Model static class Vis.D_public
          public nested model class
@Model protected static class Vis.EM_protected
          protected nested model enum
@Model static class Vis.EM_public
          public nested model enum
@Model protected static interface Vis.IM_protected
          protected nested model interface
@Model static interface Vis.IM_public
          public nested model interface
 
Nested classes/interfaces inherited from class tp.PVis
PVis.Ap_protected, PVis.Ap_public, PVis.Cp_protected, PVis.Cp_public, PVis.EP_protected, PVis.EP_public, PVis.Ip_protected, PVis.Ip_public
Inherited JML model classes and interfaces: tp.PVis.AMp_protected, tp.PVis.AMp_public, tp.PVis.Dp_protected, tp.PVis.Dp_public, tp.PVis.EMp_protected, tp.PVis.EMp_public, tp.PVis.IMp_protected, tp.PVis.IMp_public
 
Field Summary
Modifier and Type Field and Description
protected  int i_protected
          protected field
 int i_public
          public field
protected  int is_protected
           
 int is_public
           
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Ghost protected  int g_protected
          protected ghost field
@Ghost  int g_public
          public ghost field
 
Fields inherited from class tp.PVis
ip_protected, ip_public
Inherited JML ghost and model fields: gp_protected, gp_public
 
Constructor Summary
Modifier Constructor and Description
  Vis()
          public constructor
protected Vis(int i)
          protected constructor
 
JML Model Constructor Summary
Modifier Constructor and Description
protected Vis(float i)
          protected model constructor
  Vis(java.lang.Object o)
          public model constructor
 
Method Summary
Modifier and Type Method and Description
protected  void m_protected()
          protected method
 void m_public()
          public method
protected  void ms_protected()
           
 void ms_public()
           
 
JML Model Method Summary
Modifier and Type Method and Description
@Model protected  void q_protected()
          protected model method
@Model  void q_public()
          public model method
 
Methods inherited from class tp.PVis
mp_protected, mp_public
Inherited JML model methods: qp_protected, qp_public
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

i_public

public int i_public
public field


i_protected

protected int i_protected
protected field


is_public

public int is_public

is_protected

protected int is_protected
JML Ghost Field Detail

g_public

@Ghost
public int g_public
public ghost field

JML Specifications: @Ghost



g_protected

@Ghost
protected int g_protected
protected ghost field

JML Specifications: @Ghost


Constructor Detail

Vis

public Vis()
public constructor



Vis

protected Vis(int i)
protected constructor


JML Model Constructor Detail

Vis

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


JML Constructor Specifications: @Model


Vis

@Model
protected Vis(float i)
protected model constructor


JML Constructor Specifications: @Model

Method Detail

m_public

public void m_public()
public method



m_protected

protected void m_protected()
protected method



ms_public

public void ms_public()

ms_protected

protected void ms_protected()
JML Model Method Detail

q_public

@Model
public void q_public()
public model method


JML Method Specifications: @Model


q_protected

@Model
protected void q_protected()
protected model method


JML Method Specifications: @Model