Class PP

java.lang.Object
  extended by QQ
      extended by PP

public class PP
extends QQ

JML Specifications
    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; 
 


Field Summary
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
           
 
JML Ghost and Model Field Summary
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 Summary
Constructor and Description
PP()
           
 
Method Summary
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)
           
 
JML Model Method Summary
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

i

int i
JML 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; 

b

boolean b

o

java.lang.Object o

p

PP p
JML Specifications:
    maps p.i \into modelM; 

a

int[] a

list

java.util.List list
JML Model Field Detail

modelM

@Model
int modelM
 

JML Specifications: @Model

    represents modelM = 20; 

modelMZ

@Model
int modelMZ
 

JML Specifications: @Model

    private represents modelMZ = 20; 

modelM2

@Model
int modelM2
 

JML Specifications: @Model

    in modelM; 
Constructor Detail

PP

public PP()

Method Detail

m

int m()

JML Method Specifications: @Pure


mq

@Pure
int mq(int a,
            boolean b,
            java.lang.Object o)

JML Method Specifications: @Pure


mm

int mm()

JML Method Specifications:
    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); 

qq

void qq()

JML Method Specifications:
    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; 

qq1

void qq1()

JML Method Specifications:
    signals_only Exception, java.lang.RuntimeException; 

qq2

void qq2()

JML Method Specifications:
    signals_only \nothing; 

sp

void sp()

JML Method Specifications:
    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; 

z

void z(int k)

JML Method Specifications:
  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; 
  }

q0

public void q0(int i)


q1

public void q1(int i)
Javadoc comment only. Second sentence.



q2

public void q2(int i)
Parameters:
i - tag only


q3

public void q3(int i)
Javadoc comment and tag. Second sentence.

Parameters:
i - tag comment


q4

public void q4(int i)

JML Method Specifications:
    requires i > 0; 

q5

public void q5(int i)
Javadoc comment and JML. Second sentence.


JML Method Specifications:
    requires i > 0; 

q6

public void q6(int i)
Parameters:
i - tag and JML

JML Method Specifications:
    requires i > 0; 

q7

public void q7(int i)
Javadoc comment and tag and JML. Second sentence.

Parameters:
i - tag comment

JML Method Specifications:
    requires i > 0; 
JML Model Method Detail

mq0

@Model
public void mq0(int i)

JML Method Specifications: @Model


mq1

@Model
public void mq1(int i)
Javadoc comment only. Second sentence.


JML Method Specifications: @Model


mq2

@Model
public void mq2(int i)
Parameters:
i - tag only

JML Method Specifications: @Model


mq3

@Model
public void mq3(int i)
Javadoc comment and tag. Second sentence.

Parameters:
i - tag comment

JML Method Specifications: @Model


mq4

@Model
public void mq4(int i)

JML Method Specifications: @Model
    requires i > 0; 

mq5

@Model
public void mq5(int i)

JML Method Specifications: @Model
    requires i > 0; 

mq6

@Model
public void mq6(int i)

JML Method Specifications: @Model
    requires i > 0; 

mq7

@Model
public void mq7(int i)

JML Method Specifications: @Model
    requires i > 0; 

mmq5

@Model
public void mmq5(int i)
Javadoc comment and JML. Second sentence.


JML Method Specifications: @Model
    requires i > 0; 

mmq6

@Model
public void mmq6(int i)
Parameters:
i - tag and JML

JML Method Specifications: @Model
    requires i > 0; 

mmq7

@Model
public void mmq7(int i)
Javadoc comment and tag and JML. Second sentence.

Parameters:
i - tag comment

JML Method Specifications: @Model
    requires i > 0;