dafny/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy at master · Dargones/dafny · GitHub

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
@Compile(false)
module Std.PythonConcurrent replaces Concurrent {

  class {:extern} MutableMap<K(==), V(==)> ... {

    @Axiom
    constructor {:extern} (ghost inv: (K, V) -> bool, bytesKeys: bool)

    ghost predicate Valid()
    {
      true
    }

    @Axiom
    method {:extern} Keys() returns (keys: set<K>)

    @Axiom
    method {:extern} HasKey(k: K) returns (used: bool)

    @Axiom
    method {:extern} Values() returns (values: set<V>)

    @Axiom
    method {:extern} Items() returns (items: set<(K,V)>)

    @Axiom
    method {:extern} Put(k: K, v: V)

    @Axiom
    method {:extern} Get(k: K) returns (r: Option<V>)

    @Axiom
    method {:extern} Remove(k: K)

    @Axiom
    method {:extern} Size() returns (c: nat)

  }

  class {:extern} AtomicBox<T> ... {

    @Axiom
    constructor {:extern} (ghost inv: T -> bool, t: T)

    ghost predicate Valid() { true }

    @Axiom
    method {:extern} Get() returns (t: T)

    @Axiom
    method {:extern} Put(t: T)

  }

  class {:extern} Lock ... {

    @Axiom
    constructor {:extern} ()

    @Axiom
    method {:extern} Lock()

    @Axiom
    method {:extern} Unlock()

  }
}