summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b3.dfy
blob: e3a91ab29d0b9d893fb385b852d31bacc97fdd34 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
// Note:  We used integers instead of a generic Comparable type, because
// Dafny has no way of saying that the Comparable type's AtMost function
// is total and transitive.

// Note:  We couldn't get things to work out if we used the Get method.
// Instead, we used .contents.

// Note:  Due to infelicities of the Dafny sequence treatment, we
// needed to supply two lemmas, do a complicated assignment of 
// pperm, had to write invariants over p and perm rather than pperm and we couldn't use 
// "x in p".

//would be nice if we could mark pperm as a ghost variable

class Queue<T> {
  var contents: seq<T>;
  method Init();
    modifies this;
    ensures |contents| == 0;
  method Enqueue(x: T);
    modifies this;
    ensures contents == old(contents) + [x];
  method Dequeue() returns (x: T);
    requires 0 < |contents|;
    modifies this;
    ensures contents == old(contents)[1..] && x == old(contents)[0];
  function method Head(): T
    requires 0 < |contents|;
    reads this;
  { contents[0] }
  function method Get(i: int): T
    requires 0 <= i && i < |contents|;
    reads this;
  { contents[i] }
}

class Comparable {
  function AtMost(c: Comparable): bool;
    reads this, c;
}


class Benchmark3 {


  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
    requires q != null;
    modifies q;
    ensures r != null && fresh(r);
    ensures |r.contents| == |old(q.contents)|;
    ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
                r.Get(i) <= r.Get(j));
    //perm is a permutation
   ensures |perm| == |r.contents|; // ==|pperm|
   ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| );
   ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); 
   // the final Queue is a permutation of the input Queue
  ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
  {
    r := new Queue<int>;
    call r.Init();
    var p:= [];
    
    var n := 0;
	while (n < |q.contents|)
		invariant n <=|q.contents| ;
		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
		invariant n == |p|;
		decreases |q.contents| -n;
   {
		p := p + [n];
		n := n + 1;
   }
   perm:= [];
   var pperm := p + perm; 
   
    while (|q.contents| != 0)
      invariant |r.contents| == |old(q.contents)| - |q.contents|;
      invariant (forall i, j :: 0 <= i && i < j && j < |r.contents| ==>
                    r.contents[i] <= r.contents[j]);
      invariant (forall i, j ::
                    0 <= i && i < |r.contents| &&
                    0 <= j && j < |q.contents|
                    ==> r.contents[i] <= q.contents[j]);
                    
      // pperm is a permutation
      invariant   pperm == p + perm && |p| == |q.contents| && |perm| == |r.contents|;
      invariant (forall i: int :: 0 <= i && i < |perm| ==> 0 <= perm[i] && perm[i] < |pperm|);
      invariant (forall i: int :: 0 <= i && i < |p| ==> 0 <= p[i] && p[i] < |pperm|);
       invariant (forall i, j: int :: 0 <= i && i < j && j < |pperm| ==> pperm[i] != pperm[j]);
      // the current array is that permutation of the input array
      invariant (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);
      invariant (forall i: int :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);
   
    decreases |q.contents|;
    {  
      call m,k := RemoveMin(q);
      perm := perm + [p[k]]; //adds  index of min to perm
      p := p[k+1..]+ p[..k]; //remove index of min from p  
      call r.Enqueue(m);
      pperm:=  pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];
    }
    assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
   }
  
  

  method RemoveMin(q: Queue<int>) returns (m: int, k:int) //m is the min, k is m's index in q
    requires q != null && |q.contents| != 0;
    modifies q;
    ensures |old(q.contents)| == |q.contents| + 1;
    ensures  0 <= k && k < |old(q.contents)| && old(q.contents[k]) == m;
    ensures (forall i :: 0 <= i && i < |q.contents| ==> m <= q.contents[i]);
    ensures q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];  
  {
    var n := |q.contents|;
    k := 0;
    m := q.Head(); 
    var j := 0;
   
    while (j <n)
      invariant j <= n;
      invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
      invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
      invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far   
      decreases n-j;
    {
		call x:= q.Dequeue();
		call q.Enqueue(x);
		if ( x < m) {k := j; m := x;}
		j:= j+1;
		
    }
    
      j := 0;
    while (j < k)
      invariant j <= k;
      invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 
      decreases k-j;
    {     
      call x := q.Dequeue();
      call q.Enqueue(x);
      j:= j +1;
    }
    
     call m:= q.Dequeue();
   }
}