|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectA
@Pure public class A extends java.lang.Object
Documentation of class A
|
---|
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; |
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
|
|
|
---|---|
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
|
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
|
|
|
---|---|
Modifier and Type | Field and Description |
@Secret
@Model
int |
i
Documentation for a model field |
@Model
@Secret
org.jmlspecs.lang.JMLDataGroup |
q
|
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 |
|
---|
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)
|
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 |
---|
public A a
@Secret public java.lang.Object fbothJML Specifications: @NonNull @Secret
in i; maps a.i \into i;
@Secret public java.lang.Object fannot_nodocsJML Specifications: @NonNull @Secret
in i;
protected java.lang.Object fnone_nodocs
@Secret public java.lang.Object fclauses_nodocsJML Specifications: @Secret
in i; maps a.i \into i;
public int z_public
JML Model Field Detail |
---|
@Secret @Model public int i
JML Specifications: @Secret @Model
@Secret represents i = 0;
@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 |
---|
public A()
requires true;
public A(@Nullable java.lang.Object o, java.lang.Object oo)
JML Model Constructor Detail |
---|
@Model public A(int i)
requires i == 0;
@Model public A(float i)
requires i == 0.0;
@Model public A(java.lang.Object i)
requires i == null;
@Model public A(int i, int j, @NonNull java.lang.Object k, @NonNull java.lang.Object m)
@Model public A(float nodocs, int j, int k)
requires j >= 0;
Method Detail |
---|
@Deprecated public void nodocnospecs()
public void docnospecs()
@Pure public int m(@NonNull java.lang.Object o)
requires true; ensures \result == 0; signals (java.io.FileNotFoundException e) true; signals_only java.io.FileNotFoundException;
public int mmod(@NonNull java.lang.Object o)
requires true; ensures \result == 0; assignable a; signals (java.io.FileNotFoundException e) true; signals_only java.io.FileNotFoundException;
@Pure public int mm(java.lang.Object o)
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;
@NonNull public java.lang.Object n(java.lang.String s)
public java.lang.Object nn(java.lang.String s)
s
- input@Query public void q()
public normal_behavior requires true; ensures true; public behavior requires false; ensures false;
public void tttt(@NonNull java.lang.Object a, java.lang.Object b, java.lang.Object c, @Nullable java.lang.Object d)
public int mm()
|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |