blob: f24b65c6451faa08108b5bee9bb355a6ff48f247 (
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
|
//-----------------------------------------------------------------------------
//
// 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.Set, 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);
}
}
}
|
