Class A

java.lang.Object
  extended by A

@Pure
public class A
extends java.lang.Object

Documentation of class A

JML Specifications
    invariant true; 
    constraint false; 
    initially true; 
    axiom true; 
JML Specifications inherited from BB:
    invariant false; 
JML Specifications inherited from BInterface:
    invariant false; 
JML Specifications inherited from BEInterface:
    invariant false && false; 
 


Nested Class Summary
Modifier and Type Class and Description
static interface A.Annot
           
@Pure static class A.B
          DOcumentation for class B.
@Pure static interface A.BNInterface_nodoc
           
static class A.consts
           
static class BB.BBB
           
 
JML Nested Model Class Summary
Modifier and Type Class and Description
@Model static interface A.BMInterface
          Documentation for a model nested interface.
@Model static interface A.MAnnot
          Model annotation
@Model static class A.MB
          Documentation for a model nested class but not BNInterface.
@Model static class A.MC
           
 
Field Summary
Modifier and Type Field and Description
 A a
          Documentatino for a ghost field and for fboth
@Secret  java.lang.Object fannot_nodocs
           
@Secret  java.lang.Object fboth
           
@Secret  java.lang.Object fclauses_nodocs
           
protected  java.lang.Object fnone_nodocs
           
 int z_public
           
 
JML Ghost and Model Field Summary
Modifier and Type Field and Description
@Secret @Model  int i
          Documentation for a model field
@Model @Secret  org.jmlspecs.lang.JMLDataGroup q
           
 
Constructor Summary
Constructor and Description
A()
          Documentation of a constructor with specs
A(@Nullable java.lang.Object o, java.lang.Object oo)
          Documentation of a constructor without specs
 
JML Model Constructor Summary
Constructor and Description
A(float i)
           
A(float nodocs, int j, int k)
           
A(int i)
          Documentation for a model constructor with specs.
A(int i, int j, @NonNull java.lang.Object k, @NonNull java.lang.Object m)
          Documentation for a model constructor with no specs.
A(java.lang.Object i)
           
 
Method Summary
Modifier and Type Method and Description
 void docnospecs()
          Doc but no specs
@Pure  int m(@NonNull java.lang.Object o)
          Documentation of method m with specs.
 int mm()
           
@Pure  int mm(java.lang.Object o)
           
 int mmod(@NonNull java.lang.Object o)
          Documentation of method m with specs.
@NonNull  java.lang.Object n(java.lang.String s)
           
 java.lang.Object nn(java.lang.String s)
           
@Deprecated  void nodocnospecs()
          Deprecated. 
@Query  void q()
           
 void tttt(@NonNull java.lang.Object a, java.lang.Object b, java.lang.Object c, @Nullable java.lang.Object d)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

a

public A a
Documentatino for a ghost field and for fboth


fboth

@Secret
public java.lang.Object fboth
JML Specifications: @NonNull @Secret
    in i; 
    maps a.i \into i; 

fannot_nodocs

@Secret
public java.lang.Object fannot_nodocs
JML Specifications: @NonNull @Secret
    in i; 

fnone_nodocs

protected java.lang.Object fnone_nodocs

fclauses_nodocs

@Secret
public java.lang.Object fclauses_nodocs
JML Specifications: @Secret
    in i; 
    maps a.i \into i; 

z_public

public int z_public
JML Model Field Detail

i

@Secret
@Model
public int i
Documentation for a model field

JML Specifications: @Secret @Model

    @Secret 
represents i = 0; 

q

@Model
@Secret
public org.jmlspecs.lang.JMLDataGroup q
 

JML Specifications: @Model @Secret


Represents clauses for parent class model fields

    bb_model: represents bb_model = 0;

Constructor Detail

A

public A()
Documentation of a constructor with specs


JML Constructor Specifications:
    requires true; 

A

public A(@Nullable
         java.lang.Object o,
         java.lang.Object oo)
Documentation of a constructor without specs


JML Model Constructor Detail

A

@Model
public A(int i)
Documentation for a model constructor with specs.


JML Constructor Specifications: @Model
    requires i == 0; 

A

@Model
public A(float i)

JML Constructor Specifications: @Model
    requires i == 0.0; 

A

@Model
public A(java.lang.Object i)

JML Constructor Specifications: @Model
    requires i == null; 

A

@Model
public A(int i,
               int j,
               @NonNull
               java.lang.Object k,
               @NonNull
               java.lang.Object m)
Documentation for a model constructor with no specs.


JML Constructor Specifications: @Model


A

@Model
public A(float nodocs,
               int j,
               int k)

JML Constructor Specifications: @Model
    requires j >= 0; 
Method Detail

nodocnospecs

@Deprecated
public void nodocnospecs()
Deprecated. 

Documentation for a model method mdl_nospecs and for nodocnospecs



docnospecs

public void docnospecs()
Doc but no specs



m

@Pure
public int m(@NonNull
                  java.lang.Object o)
Documentation of method m with specs. More info.


JML Method Specifications: @Pure
    requires true; 
    ensures \result == 0; 
    signals (java.io.FileNotFoundException e) true; 
    signals_only java.io.FileNotFoundException; 

mmod

public int mmod(@NonNull
                java.lang.Object o)
Documentation of method m with specs. More info.


JML Method Specifications:
    requires true; 
    ensures \result == 0; 
    assignable a; 
    signals (java.io.FileNotFoundException e) true; 
    signals_only java.io.FileNotFoundException; 

mm

@Pure
public int mm(java.lang.Object o)

JML Method Specifications: @Pure
    requires true; 
    ensures \result == 0; 
    signals (java.io.FileNotFoundException e) true; 
    signals_only java.io.FileNotFoundException; 
JML Specifications inherited from BB:
    ensures z_public == 10; 
JML Specifications inherited from BInterface:
    ensures false; 
JML Specifications inherited from BEInterface:
    ensures false && false; 

n

@NonNull
public java.lang.Object n(java.lang.String s)

JML Method Specifications: @NonNull


nn

public java.lang.Object nn(java.lang.String s)
Parameters:
s - input
Returns:
output

JML Method Specifications: @NonNull


q

@Query
public void q()

JML Method Specifications: @Query
  public normal_behavior
    requires true; 
    ensures true; 
  public behavior
    requires false; 
    ensures false; 

tttt

public void tttt(@NonNull
                 java.lang.Object a,
                 java.lang.Object b,
                 java.lang.Object c,
                 @Nullable
                 java.lang.Object d)


mm

public int mm()