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
static interface SVis.As_public
          public nested annotation
static class SVis.Cs_public
          private model constructor
static class SVis.ES_public
           
static interface SVis.Is_public
          public nested interface
static interface Vis.A_public
          public nested annotation
static class Vis.C_public
          public nested class
static class Vis.E_public
          public nested enum
static interface Vis.I_public
          public nested interface
 
JML Nested Model Class Summary
Modifier and Type Class and Description
@Model static interface Vis.AM_public
          public nested model annotation
@Model static class Vis.D_public
          public nested model class
@Model static class Vis.EM_public
          public nested model enum
@Model static interface Vis.IM_public
          public nested model interface
 
Nested classes/interfaces inherited from class tp.PVis
PVis.Ap_public, PVis.Cp_public, PVis.EP_public, PVis.Ip_public
Inherited JML model classes and interfaces: tp.PVis.AMp_public, tp.PVis.Dp_public, tp.PVis.EMp_public, tp.PVis.IMp_public
 
Field Summary
Modifier and Type Field and Description
 int i_public
          public field
 int is_public
           
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Ghost  int g_public
          public ghost field
 
Fields inherited from class tp.PVis
ip_public
Inherited JML ghost and model fields: gp_public
 
Constructor Summary
Constructor and Description
Vis()
          public constructor
 
JML Model Constructor Summary
Constructor and Description
Vis(java.lang.Object o)
          public model constructor
 
Method Summary
Modifier and Type Method and Description
 void m_public()
          public method
 void ms_public()
           
 
JML Model Method Summary
Modifier and Type Method and Description
@Model  void q_public()
          public model method
 
Methods inherited from class tp.PVis
mp_public
Inherited JML model methods: qp_public
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

i_public

public int i_public
public field


is_public

public int is_public
JML Ghost Field Detail

g_public

@Ghost
public int g_public
public ghost field

JML Specifications: @Ghost


Constructor Detail

Vis

public Vis()
public constructor


JML Model Constructor Detail

Vis

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


JML Constructor Specifications: @Model

Method Detail

m_public

public void m_public()
public method



ms_public

public void ms_public()
JML Model Method Detail

q_public

@Model
public void q_public()
public model method


JML Method Specifications: @Model