|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPP
public class PP extends QQ
|
---|
invariant i + 2 * 3 - 4 / 5 + 6 % i + (i << 5) + (i >> 6) + (i >>> i) == -10; invariant i > 0 && i < 0 && i == 0 && (i <= +10 ? i >= 0 : i != 0); invariant b || !b && (b ==> b) && (b <==> b) && (b <=!=> b) && (b <== b); invariant (i & 1) + (i ^ 1) + (i | 1) + (~i) == 0; invariant \type(int) <: \typeof(o); invariant \type(int) <#= \typeof(o); invariant \type(int) <# \typeof(o); invariant o instanceof java.lang.String; invariant true && false && (i == 10.0) && (i < -100000.0) && (i > +40000.0) && (i > +4.0E49); invariant "asd" != (Object)null && 'c' != 'd' && 'a' != '%' && "45" != "\n\"\'\u001c"; invariant (int)9 == 9 && (char)3 == 'd' && (float)4 == (double)5 && (short)1 == (byte)(-1) && (long)-13 == -12; invariant (new int[]{1, 2, 3}).length == 3 && (new int[]{1, 2, 3})[0] == 1 && a[3] == 6; invariant (new PP()).i == 0; invariant (\forall int i; ; i != 0) && (\forall int k; k > 0; k > -1); invariant (\exists int i; ; i != 0) && (\exists int k; k > 0; k > -1); invariant (\num_of int i; ; i == 0) == (\num_of int k; k > 0; k > -1); invariant (\max int i; i > 0 && i < 10; i) == (\min int i; i > 0 && i < 10; i); invariant (\sum int i; i > 0 && i < 10; i) == (\product int i; i > 0 && i < 10; i); invariant this.i == 0 && super.bb() && PP.class != null; invariant (* informal predicate *) && false && m() == 0 && 0 == mq(1, false, new Object()); invariant \is_initialized(PP); invariant \is_initialized(Integer); invariant \invariant_for(o); invariant (\lblpos A true); invariant (\lblneg A true); invariant (\lbl A true); invariant !\reach(o).isEmpty(); invariant \reach(o) != null; invariant (new PP(){ () { super(); } int m() { return 5; } }) != null; invariant new JMLSetType { Integer o | list.contains(o) && o > 0 } != null; constraint i >= \old(i); axiom true; initially true; readable i if true; writable i if true; monitors_for i = o; public invariant false; public constraint i >= \old(i); public initially true; public readable i if true; public writable i if true; public monitors_for i = o; |
Modifier and Type | Field and Description |
---|---|
(package private) int[] |
a
|
(package private) boolean |
b
|
(package private) int |
i
|
(package private) java.util.List |
list
|
(package private) java.lang.Object |
o
|
(package private) PP |
p
|
|
|
---|---|
Modifier and Type | Field and Description |
@Model
(package private) int |
modelM
|
@Model
(package private) int |
modelM2
|
@Model
(package private) int |
modelMZ
|
Fields inherited from class QQ |
---|
qq |
Constructor and Description |
---|
PP()
|
Modifier and Type | Method and Description |
---|---|
(package private) int |
m()
|
(package private) int |
mm()
|
@Pure
(package private) int |
mq(int a,
boolean b,
java.lang.Object o)
|
void |
q0(int i)
|
void |
q1(int i)
Javadoc comment only. |
void |
q2(int i)
|
void |
q3(int i)
Javadoc comment and tag. |
void |
q4(int i)
|
void |
q5(int i)
Javadoc comment and JML. |
void |
q6(int i)
|
void |
q7(int i)
Javadoc comment and tag and JML. |
(package private) void |
qq()
|
(package private) void |
qq1()
|
(package private) void |
qq2()
|
(package private) void |
sp()
|
(package private) void |
z(int k)
|
|
|
---|---|
Modifier and Type | Method and Description |
@Model
void |
mmq5(int i)
Javadoc comment and JML. |
@Model
void |
mmq6(int i)
|
@Model
void |
mmq7(int i)
Javadoc comment and tag and JML. |
@Model
void |
mq0(int i)
|
@Model
void |
mq1(int i)
Javadoc comment only. |
@Model
void |
mq2(int i)
|
@Model
void |
mq3(int i)
Javadoc comment and tag. |
@Model
void |
mq4(int i)
|
@Model
void |
mq5(int i)
|
@Model
void |
mq6(int i)
|
@Model
void |
mq7(int i)
|
Methods inherited from class QQ |
---|
bb |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
int iJML Specifications:
readable i if true; writable i if true; monitors_for i = o; public readable i if true; public writable i if true; public monitors_for i = o;
boolean b
java.lang.Object o
PP pJML Specifications:
maps p.i \into modelM;
int[] a
java.util.List list
JML Model Field Detail |
---|
@Model int modelM
JML Specifications: @Model
represents modelM = 20;
@Model int modelMZ
JML Specifications: @Model
private represents modelMZ = 20;
@Model int modelM2
JML Specifications: @Model
in modelM;
Constructor Detail |
---|
public PP()
Method Detail |
---|
int m()
@Pure int mq(int a, boolean b, java.lang.Object o)
int mm()
ensures \result > 0 && !\nonnullelements(a) && \elemtype(\typeof(a)) == \type(int); ensures \duration(m()) > 0 && \space(o) > 0 && \working_space(m()) > 0; ensures \fresh(a) && \fresh(a, o); ensures \max(\lockset) == a; ensures \max(\lockset).hashCode() != 0; ensures \not_modified(i,o); ensures \not_modified(a[1 .. *]); ensures \not_assigned(\nothing) || \only_accessed(\nothing) || \only_captured(\nothing) || \only_assigned(\nothing); ensures \not_assigned(\everything) || \only_accessed(\everything) || \only_captured(\everything) || \only_assigned(\everything); ensures \not_assigned(i) || \only_accessed(i) || \only_captured(i) || \only_assigned(i); ensures \not_assigned(i,a[1 .. *]) || \only_accessed(i,a[1 .. *]) || \only_captured(i,a[*]) || \only_assigned(i,o.*); ensures \not_assigned(\not_specified) || \only_accessed(\not_specified) || \only_captured(\not_specified) || \only_assigned(\not_specified);
void qq()
requires \same; requires true; requires true; ensures false; ensures true; signals (Exception e) true; signals (Exception) false; signals_only Exception; diverges true; assignable i; assignable \nothing; assignable p.i, p.*, this.*, super.*, PP.*; assignable i, o, a, a[*], a[1], a[1 .. 2], a[1 .. *], a[1 .. *]; assignable \everything; accessible \nothing; accessible \everything; accessible i, PP.*; CALLABLE \nothing; CALLABLE \everything; CALLABLE, , , , , ; measured_by 10; measured_by 20 if false; captures i, a[*]; captures \nothing; captures \everything; duration 0; duration 0 if true; working_space 0; working_space 0 if true; when false;
void qq1()
signals_only Exception, java.lang.RuntimeException;
void qq2()
signals_only \nothing;
void sp()
requires \not_specified; ensures \not_specified; diverges \not_specified; signals (Exception) \not_specified; assignable \not_specified; accessible \not_specified; CALLABLE \not_specified; when \not_specified; measured_by \not_specified; duration \not_specified; working_space \not_specified; captures \not_specified;
void z(int k)
public normal_behavior requires true; {| ensures false; diverges true; also ensures true; diverges true; |} protected exceptional_behavior forall Object o; old int j = k + 1; requires false; signals (Exception) true; code behavior requires false; signals (Exception) true; private code model_program { } model_program { int x = 0; x++; ++x; x--; --x; x = 1; x += 1; x -= 1; x *= 1; x /= 1; x %= 1; x <<= 1; x >>= 1; x >>>= 1; x |= 1; x &= 1; x ^= 1; if (true) x = 1; if (true) { x = 1; } else { x = 2; } while (true) { x = 1; if (x == 2) continue; if (x == 3) break; } do x = 1; while (true); switch (x) { case 1: x = 2; break; default: x = 3; } ; assume Assume true; assert Assert true; behavior requires true; ensures false; abrupt_behavior requires false; continues true; breaks true; returns true; invariant false; }
public void q0(int i)
public void q1(int i)
public void q2(int i)
i
- tag onlypublic void q3(int i)
i
- tag commentpublic void q4(int i)
requires i > 0;
public void q5(int i)
requires i > 0;
public void q6(int i)
i
- tag and JMLrequires i > 0;
public void q7(int i)
i
- tag commentrequires i > 0;
JML Model Method Detail |
---|
@Model public void mq0(int i)
@Model public void mq1(int i)
@Model public void mq2(int i)
i
- tag only@Model public void mq3(int i)
i
- tag comment@Model public void mq4(int i)
requires i > 0;
@Model public void mq5(int i)
requires i > 0;
@Model public void mq6(int i)
requires i > 0;
@Model public void mq7(int i)
requires i > 0;
@Model public void mmq5(int i)
requires i > 0;
@Model public void mmq6(int i)
i
- tag and JMLrequires i > 0;
@Model public void mmq7(int i)
i
- tag commentrequires i > 0;
|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |