Class Vis

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

public class Vis
extends SVis


Nested Class Summary
Modifier and Type Class and Description
(package private) static interface Vis.A_package
          package nested annotation
private static interface Vis.A_private
          private nested annotation
protected static interface Vis.A_protected
          protected nested annotation
static interface Vis.A_public
          public nested annotation
(package private) static class Vis.C_package
          package nested class
private static class Vis.C_private
          private nested class
protected static class Vis.C_protected
          protected nested class
static class Vis.C_public
          public nested class
(package private) static class Vis.E_package
          package nested enum
private static class Vis.E_private
          private nested enum
protected static class Vis.E_protected
          protected nested enum
static class Vis.E_public
          public nested enum
(package private) static interface Vis.I_package
          package nested interface
private static interface Vis.I_private
          private nested interface
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 (package private) static interface Vis.AM_package
          package nested model annotation
@Model private static interface Vis.AM_private
          private nested model annotation
@Model protected static interface Vis.AM_protected
          protected nested model annotation
@Model static interface Vis.AM_public
          public nested model annotation
@Model (package private) static class Vis.D_package
          package nested model class
@Model private static class Vis.D_private
          private nested model class
@Model protected static class Vis.D_protected
          protected nested model class
@Model static class Vis.D_public
          public nested model class
@Model (package private) static class Vis.EM_package
          package nested model enum
@Model private static class Vis.EM_private
          private nested model enum
@Model protected static class Vis.EM_protected
          protected nested model enum
@Model static class Vis.EM_public
          public nested model enum
@Model (package private) static interface Vis.IM_package
          package nested model interface
@Model private static interface Vis.IM_private
          private nested model interface
@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 SVis
SVis.As_package, SVis.As_protected, SVis.As_public, SVis.Cs_package, SVis.Cs_protected, SVis.Cs_public, SVis.ES_package, SVis.ES_protected, SVis.ES_public, SVis.Is_package, SVis.Is_protected, SVis.Is_public
Inherited JML model classes and interfaces: SVis.AMs_package, SVis.AMs_protected, SVis.AMs_public, SVis.Ds_package, SVis.Ds_protected, SVis.Ds_public, SVis.EMs_package, SVis.EMs_protected, SVis.EMs_public, SVis.IMs_package, SVis.IMs_protected, SVis.IMs_public
 
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
(package private)  int i_package
          package field
private  int i_private
          private field
protected  int i_protected
          protected field
 int i_public
          public field
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Ghost (package private)  int g_package
          package ghost field
@Ghost private  int g_private
          private ghost field
@Ghost protected  int g_protected
          protected ghost field
@Ghost  int g_public
          public ghost field
 
Fields inherited from class SVis
is_package, is_protected, is_public
Inherited JML ghost and model fields: gs_package, gs_protected, gs_public
 
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
(package private) Vis(int i, int j)
          package constructor
private Vis(int i, int j, int k)
          private constructor
 
JML Model Constructor Summary
Modifier Constructor and Description
protected Vis(float i)
          protected model constructor
(package private) Vis(float i, float j)
          package model constructor
private Vis(float i, float j, float k)
          private model constructor
  Vis(java.lang.Object o)
          public model constructor
 
Method Summary
Modifier and Type Method and Description
(package private)  void m_package()
          package method
private  void m_private()
          private method
protected  void m_protected()
          protected method
 void m_public()
          public method
 
JML Model Method Summary
Modifier and Type Method and Description
@Model (package private)  void q_package()
          package model method
@Model private  void q_private()
          private model method
@Model protected  void q_protected()
          protected model method
@Model  void q_public()
          public model method
 
Methods inherited from class SVis
ms_package, ms_protected, ms_public
Inherited JML model methods: qs_package, qs_protected, qs_public
 
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


i_package

int i_package
package field


i_private

private int i_private
private field

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



g_package

@Ghost
int g_package
package ghost field

JML Specifications: @Ghost



g_private

@Ghost
private int g_private
private ghost field

JML Specifications: @Ghost


Constructor Detail

Vis

public Vis()
public constructor



Vis

protected Vis(int i)
protected constructor



Vis

Vis(int i,
    int j)
package constructor



Vis

private Vis(int i,
            int j,
            int k)
private 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


Vis

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


JML Constructor Specifications: @Model


Vis

@Model
private Vis(float i,
                  float j,
                  float k)
private model constructor


JML Constructor Specifications: @Model

Method Detail

m_public

public void m_public()
public method



m_protected

protected void m_protected()
protected method



m_package

void m_package()
package method



m_private

private void m_private()
private method


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


q_package

@Model
void q_package()
package model method


JML Method Specifications: @Model


q_private

@Model
private void q_private()
private model method


JML Method Specifications: @Model