0
# DafnyRuntimePython
1

2
The Python runtime library for Dafny, a verification-ready programming language that compiles to multiple target languages. This runtime enables Dafny language features in Python by providing essential data structures, type representations, mathematical operations, control flow constructs, and utility functions needed to execute Dafny-compiled Python code.
3

4
## Package Information
5

6
- **Package Name**: DafnyRuntimePython
7
- **Language**: Python
8
- **Installation**: `pip install DafnyRuntimePython`
9
- **Minimum Python Version**: 3.8+
10

11
## Core Imports
12

13
```python
14
import _dafny
15
from _dafny import Seq, Set, MultiSet, Map, Array, BigRational
16
```
17

18
For System module types:
19

20
```python
21
import System_
22
from System_ import nat
23
```
24

25
## Basic Usage
26

27
```python
28
import _dafny
29
from _dafny import Seq, Set, Map, BigRational
30

31
# Create Dafny sequences (similar to lists)
32
seq = Seq([1, 2, 3, 4, 5])
33
string_seq = Seq("hello", isStr=True)
34

35
# Work with sets
36
my_set = Set([1, 2, 3, 4])
37
subset = Set([1, 2])
38
print(subset.issubset(my_set))  # True
39

40
# Use maps (key-value pairs)
41
my_map = Map({1: 'one', 2: 'two', 3: 'three'})
42
updated_map = my_map.set(4, 'four')  # Immutable - returns new map
43

44
# High-precision rational numbers
45
big_num = BigRational(1, 3)  # 1/3 with arbitrary precision
46
result = big_num + BigRational(2, 3)  # 1.0
47

48
# String conversion with Dafny semantics
49
print(_dafny.string_of(seq))  # [1, 2, 3, 4, 5]
50
print(_dafny.string_of(string_seq))  # hello
51
```
52

53
## Architecture
54

55
The runtime library consists of two main modules:
56

57
- **`_dafny`**: Core runtime functionality including data structures, mathematical types, control flow primitives, and utility functions
58
- **`System_`**: System-level type definitions and operations
59

60
All data structures are designed to preserve Dafny's immutability semantics and type system constraints, ensuring that Dafny's verification properties are maintained in the Python execution environment.
61

62
## Capabilities
63

64
### Core Data Structures
65

66
Dafny's fundamental collection types: sequences (Seq), sets (Set), multisets (MultiSet), maps (Map), and multi-dimensional arrays (Array). These immutable data structures preserve Dafny's semantics and provide efficient operations.
67

68
```python { .api }
69
class Seq:
70
    def __init__(self, iterable=None, isStr=False): ...
71
    def __add__(self, other): ...
72
    def __getitem__(self, key): ...
73
    def set(self, key, value): ...
74

75
class Set(frozenset):
76
    def union(self, other): ...
77
    def intersection(self, other): ...
78
    def ispropersubset(self, other): ...
79

80
class MultiSet(Counter):
81
    def union(self, other): ...
82
    def intersection(self, other): ...
83
    
84
class Map(dict):
85
    def set(self, key, value): ...
86
    def __or__(self, other): ...
87

88
class Array:
89
    def __init__(self, initValue, *dims): ...
90
    def length(self, i): ...
91
```
92

93
[Core Data Structures](./data-structures.md)
94

95
### Mathematical Types
96

97
High-precision mathematical types for arbitrary precision arithmetic and ordinal number operations. Includes BigRational for exact decimal arithmetic and BigOrdinal for ordinal operations.
98

99
```python { .api }
100
class BigRational(Fraction):
101
    def __dafnystr__(self): ...
102
    def is_integer(self): ...
103
    def __add__(self, other): ...
104
    def __truediv__(self, other): ...
105

106
class BigOrdinal:
107
    @staticmethod
108
    def is_limit(ord): ...
109
    @staticmethod
110
    def is_succ(ord): ...
111
    @staticmethod
112
    def is_nat(ord): ...
113
```
114

115
[Mathematical Types](./mathematical-types.md)
116

117
### Control Flow and Exceptions
118

119
Exception-driven control flow constructs for implementing Dafny's labeled break/continue statements, tail call optimization, and program halting. Includes context managers for proper exception handling.
120

121
```python { .api }
122
class Break(Exception):
123
    target: str
124

125
class Continue(Exception):
126
    target: str
127

128
class TailCall(Exception): pass
129

130
class HaltException(Exception):
131
    message: str
132

133
def label(name: str = None): ...
134
def c_label(name: str = None): ...
135
```
136

137
[Control Flow](./control-flow.md)
138

139
### Utility Functions
140

141
String conversion, character arithmetic, mathematical operations, and generator functions. These utilities handle Dafny-specific string representations, Unicode operations, and quantification over collections.
142

143
```python { .api }
144
def string_of(value) -> str: ...
145
def string_from_utf_16(utf_16_code_units): ...
146
def plus_char(a, b): ...
147
def minus_char(a, b): ...
148
def euclidian_division(a, b): ...
149
def euclidian_modulus(a, b): ...
150
def quantifier(vals, frall, pred): ...
151
def AllBooleans(): ...
152
def AllIntegers(): ...
153
def IntegerRange(lo, hi): ...
154
```
155

156
[Utility Functions](./utilities.md)
157

158
### System Types
159

160
System-level type definitions from the System_ module, including natural number types and validation functions for Dafny's type system.
161

162
```python { .api }
163
class nat:
164
    @staticmethod
165
    def default(): ...
166
    @staticmethod
167
    def _Is(source__): ...
168
```
169

170
[System Types](./system-types.md)
171

172
## Types
173

174
### Core Types
175

176
```python { .api }
177
class CodePoint(str):
178
    escapes: dict
179
    def __escaped__(self): ...
180
    def __dafnystr__(self): ...
181
    @staticmethod
182
    def is_code_point(i): ...
183

184
class Doubler:
185
    def __init__(self, start): ...
186
    def __iter__(self): ...
187

188
class defaults:
189
    @staticmethod
190
    def bool(): ...
191
    @staticmethod
192
    def char(): ...
193
    @staticmethod
194
    def int(): ...
195
    @staticmethod
196
    def real(): ...
197

198
class classproperty(property):
199
    def __get__(self, instance, owner): ...
200
```