blob: fff0476ee0b485f2801fb730d7a962690c943061 (
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
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
namespace Microsoft.AbstractInterpretationFramework.Collections {
using System.Collections;
using System.Diagnostics.Contracts;
/// <summary>
/// Extend sets for using as a IWorkList.
/// </summary>
public class WorkSet : Microsoft.Boogie.GSet<object>, Microsoft.Boogie.IWorkList {
// See Bug #148 for an explanation of why this is here.
// Without it, the contract inheritance rules will complain since it
// has nowhere to attach the out-of-band contract it gets from
// ICollection.Count that it gets from IWorkList.
public override int Count {
get {
return base.Count;
}
}
[Pure]
public bool IsEmpty() {
return Count == 0;
}
/// <summary>
/// Pull an element out of the workset.
/// </summary>
public object Pull() {
IEnumerator iter = GetEnumerator();
iter.MoveNext();
object result = cce.NonNull(iter.Current);
Remove(result);
return result;
}
bool Microsoft.Boogie.IWorkList.Add(object o) {
if (o == null)
throw new System.ArgumentNullException();
this.Add(o);
return true;
}
bool Microsoft.Boogie.IWorkList.AddAll(IEnumerable objs) {
if (objs == null)
throw new System.ArgumentNullException();
return this.AddAll(objs);
}
// ICollection members
public void CopyTo(System.Array/*!*/ a, int i) {
//Contract.Requires(a != null);
if (this.Count > a.Length - i)
throw new System.ArgumentException();
int j = i;
foreach (object o in this) {
a.SetValue(o, j++);
}
return;
}
object/*!*/ ICollection.SyncRoot {
[Pure]
get {
Contract.Ensures(Contract.Result<object>() != null);
return this;
}
}
public bool IsSynchronized {
get {
return false;
}
}
}
}
namespace Microsoft.AbstractInterpretationFramework.Collections.Generic {
using System.Collections.Generic;
public class HashMultiset<T> {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(dict != null);
}
private readonly IDictionary<T, int>/*!*/ dict;
//Contract.Invariant(Contract.ForAll(dict , entry => entry.Value >= 1));
public HashMultiset() {
this.dict = new Dictionary<T, int>();
// base();
}
public HashMultiset(int size) {
this.dict = new Dictionary<T, int>(size);
// base();
}
public void Add(T t) {
cce.BeginExpose(this);
{
if (dict.ContainsKey(t)) {
dict[t] = dict[t] + 1;
} else {
dict.Add(t, 1);
}
}
cce.EndExpose();
}
public void Remove(T t) {
if (dict.ContainsKey(t)) {
cce.BeginExpose(this);
{
int count = dict[t];
if (count == 1) {
dict.Remove(t);
} else {
dict[t] = count - 1;
}
}
cce.EndExpose();
}
}
public bool Contains(T t) {
return dict.ContainsKey(t);
}
}
}
|
