-
Notifications
You must be signed in to change notification settings - Fork 0
/
Concurrent-notarget-cs.dfy
51 lines (28 loc) · 1.08 KB
/
Concurrent-notarget-cs.dfy
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
module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
class {:extern} MutableMap<K(==), V(==)> ... {
constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
ghost predicate Valid()
{
true
}
method {:extern} {:axiom} Keys() returns (keys: set<K>)
method {:extern} {:axiom} HasKey(k: K) returns (used: bool)
method {:extern} {:axiom} Values() returns (values: set<V>)
method {:extern} {:axiom} Items() returns (items: set<(K,V)>)
method {:extern} {:axiom} Put(k: K, v: V)
method {:extern} {:axiom} Get(k: K) returns (r: Option<V>)
method {:extern} {:axiom} Remove(k: K)
method {:extern} {:axiom} Size() returns (c: nat)
}
class {:extern} AtomicBox<T> ... {
constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
ghost predicate Valid() { true }
method {:extern} {:axiom} Get() returns (t: T)
method {:extern} {:axiom} Put(t: T)
}
class {:extern} Lock ... {
constructor {:extern} {:axiom} ()
method {:extern} {:axiom} Lock()
method {:extern} {:axiom} Unlock()
}
}