Class Name: 
kiasan.examples.Container

Report Rendered: Mon May 04 11:28:33 CDT 2009, by Sireum/Kiasan for Java v0.1.20090504

Methods Covered:
PercentRatio
Class / Method T E Instruction Coverage Branch Coverage Time
2 1
  11/11
  100%
  0/0
  100%
 0.002s
3 0
  13/13
  100%
  2/2
  100%
 0.000s
2 0
  11/11
  100%
  0/0
  100%
 0.000s
Total
 7 1
  35/35
  100%
  2/2
  100%
 0.002s
Source Code:
1   package kiasan.examples;
2   
3   public class Container<E> {
4     E data;
5   
6     void swap(final Container<E> other) {
7       final E temp = this.data;
8       this.data = other.data;
9       other.data = temp;
10    }
11  
12    void swap2(final Container<E> other) {
13      if (other != null) {
14        final E temp = this.data;
15        this.data = other.data;
16        other.data = temp;
17      }
18    }
19  
20    //@ requires other != null;
21    //@ ensures \old(this.data) == other.data && \old(other.data) == this.data;
22    void swap3(final Container<E> other) {
23      final E temp = this.data;
24      this.data = other.data;
25      other.data = temp;
26    }
27  }