tessl/pypi-dafnyruntimepython
Python runtime library for Dafny, providing essential data structures, type representations, and utility functions for executing Dafny-compiled Python code
—
Pending
data-structures.mddocs/
Core Data Structures
Dafny's fundamental collection types implemented in Python with immutability semantics and type-safe operations. These data structures preserve Dafny's verification properties and provide efficient operations for sequences, sets, multisets, maps, and arrays.
Capabilities
Sequences (Seq)
Immutable sequences that can represent both generic collections and strings. Sequences support concatenation, slicing, element access, and string-specific operations when configured as string sequences.
class Seq:
def __init__(self, iterable=None, isStr=False):
"""
Create a sequence from an iterable.
Parameters:
- iterable: Initial elements (list, string, or other iterable)
- isStr: String tracking behavior (True/False/None)
True: definitely a string
False: might be a string, apply heuristics
None: don't apply heuristics
"""
@property
def Elements(self):
"""Returns the underlying elements as a list."""
@property
def UniqueElements(self):
"""Returns frozenset of unique elements."""
def VerbatimString(self, asliteral):
"""
Returns string representation.
Parameters:
- asliteral: If True, returns quoted literal format
Returns:
str: String representation
"""
def __dafnystr__(self) -> str:
"""Returns Dafny-specific string representation."""
def __add__(self, other):
"""
Concatenates two sequences.
Parameters:
- other: Another Seq to concatenate
Returns:
Seq: New sequence containing concatenated elements
"""
def __getitem__(self, key):
"""
Gets element at index or slice.
Parameters:
- key: int index or slice object
Returns:
Element at index or new Seq for slice
"""
def set(self, key, value):
"""
Returns new sequence with element at key set to value.
Parameters:
- key: int index
- value: New value for element
Returns:
Seq: New sequence with updated element
"""
def __len__(self):
"""Returns length of sequence."""
def __hash__(self) -> int:
"""Hash based on tuple of elements."""
def __eq__(self, other) -> bool:
"""Equality comparison based on elements."""
def __lt__(self, other):
"""True if this sequence is a proper prefix of other."""
def __le__(self, other):
"""True if this sequence is a prefix of or equal to other."""Usage Examples
# Generic sequence
numbers = Seq([1, 2, 3, 4, 5])
doubled = Seq([x * 2 for x in numbers.Elements])
combined = numbers + doubled
# String sequence
text = Seq("hello world", isStr=True)
substring = text[0:5] # Seq containing "hello"
# Sequence operations
updated = numbers.set(2, 99) # [1, 2, 99, 4, 5]
print(len(numbers)) # 5
print(numbers[2]) # 3Sets (Set)
Immutable sets based on Python's frozenset with additional Dafny-specific operations. Sets provide mathematical set operations with immutable semantics.
class Set(frozenset):
@property
def Elements(self):
"""Returns the set itself."""
@property
def AllSubsets(self):
"""Returns generator yielding all subsets of this set."""
def __dafnystr__(self) -> str:
"""Returns Dafny string representation: {elem1, elem2, ...}"""
def union(self, other):
"""
Returns set union.
Parameters:
- other: Another Set or iterable
Returns:
Set: New set containing all elements from both sets
"""
def intersection(self, other):
"""
Returns set intersection.
Parameters:
- other: Another Set or iterable
Returns:
Set: New set containing common elements
"""
def ispropersubset(self, other):
"""
Tests if this set is a proper subset of other.
Parameters:
- other: Another Set
Returns:
bool: True if proper subset
"""
def __or__(self, other):
"""Union operator (|)."""
def __sub__(self, other):
"""Set difference operator (-)."""Usage Examples
# Create sets
set1 = Set([1, 2, 3, 4])
set2 = Set([3, 4, 5, 6])
# Set operations
union_set = set1.union(set2) # {1, 2, 3, 4, 5, 6}
intersection_set = set1 & set2 # {3, 4}
difference_set = set1 - set2 # {1, 2}
# Subset testing
subset = Set([1, 2])
print(subset.issubset(set1)) # True
print(subset.ispropersubset(set1)) # True
# All subsets generation
for subset in Set([1, 2]).AllSubsets:
print(subset) # {}, {1}, {2}, {1, 2}Multisets (MultiSet)
Multisets (bags) that track element multiplicities, extending Python's Counter with Dafny-specific operations and immutable semantics.
class MultiSet(Counter):
@property
def cardinality(self):
"""Total number of elements (sum of all multiplicities)."""
@property
def keys(self):
"""Set of unique elements with positive count."""
@property
def Elements(self):
"""All elements including duplicates."""
@property
def UniqueElements(self):
"""Alias for keys property."""
def __dafnystr__(self) -> str:
"""Returns Dafny string representation: multiset{elem1, elem2, ...}"""
def union(self, other):
"""
Returns multiset union (sum of multiplicities).
Parameters:
- other: Another MultiSet
Returns:
MultiSet: New multiset with combined multiplicities
"""
def intersection(self, other):
"""
Returns multiset intersection (minimum multiplicities).
Parameters:
- other: Another MultiSet
Returns:
MultiSet: New multiset with minimum multiplicities
"""
def __sub__(self, other):
"""
Returns multiset difference.
Parameters:
- other: Another MultiSet
Returns:
MultiSet: New multiset with subtracted multiplicities
"""
def isdisjoint(self, other):
"""
Tests if multisets share no common elements.
Parameters:
- other: Another MultiSet
Returns:
bool: True if no common elements
"""
def issubset(self, other):
"""
Tests if this multiset is a subset (all multiplicities ≤ other's).
Parameters:
- other: Another MultiSet
Returns:
bool: True if subset
"""
def ispropersubset(self, other):
"""
Tests if this multiset is a proper subset.
Parameters:
- other: Another MultiSet
Returns:
bool: True if proper subset
"""
def set(self, key, value):
"""
Returns new multiset with key's count set to value.
Parameters:
- key: Element to set count for
- value: New count (non-negative integer)
Returns:
MultiSet: New multiset with updated count
"""
def __contains__(self, item):
"""True if item count > 0."""
def __eq__(self, other):
"""Equality based on element counts."""
def __hash__(self):
"""Hash based on unique keys."""
def __ne__(self, other):
"""Inequality comparison (opposite of __eq__)."""
def __setattr__(self, key, value):
"""
Prevents direct attribute modification - raises TypeError.
Raises:
TypeError: Always, as MultiSet objects are immutable
Note: Use .set() method for functional updates instead
"""Usage Examples
# Create multisets
ms1 = MultiSet([1, 1, 2, 2, 2, 3]) # {1: 2, 2: 3, 3: 1}
ms2 = MultiSet([2, 2, 3, 3, 4]) # {2: 2, 3: 2, 4: 1}
# Multiset operations
union = ms1.union(ms2) # {1: 2, 2: 5, 3: 3, 4: 1}
intersection = ms1 & ms2 # {2: 2, 3: 1}
difference = ms1 - ms2 # {1: 2, 2: 1}
# Properties and testing
print(ms1.cardinality) # 6 (total elements)
print(ms1.keys) # Set({1, 2, 3})
print(1 in ms1) # True
print(ms1.issubset(union)) # True
# Update counts
updated = ms1.set(1, 5) # Set count of 1 to 5Maps (Map)
Immutable key-value mappings with Dafny semantics, providing functional-style updates and set-based views of keys, values, and items.
class Map(dict):
@property
def Elements(self):
"""Returns the map itself."""
@property
def keys(self):
"""Returns Set of keys."""
@property
def values(self):
"""Returns Set of values."""
@property
def items(self):
"""Returns Set of key-value pairs (tuples)."""
def __dafnystr__(self) -> str:
"""Returns Dafny string representation: map[key1 := val1, key2 := val2, ...]"""
def set(self, key, value):
"""
Returns new map with key-value pair added/updated.
Parameters:
- key: Key to set
- value: Value to associate with key
Returns:
Map: New map with key-value pair
"""
def __sub__(self, other):
"""
Returns map with keys from other removed.
Parameters:
- other: Iterable of keys to remove
Returns:
Map: New map without specified keys
"""
def __or__(self, other):
"""
Returns map union (other's values take precedence).
Parameters:
- other: Another Map
Returns:
Map: New map with combined key-value pairs
"""
def __hash__(self):
"""Hash based on items."""
def __setattr__(self, key, value):
"""
Prevents direct attribute modification - raises TypeError.
Raises:
TypeError: Always, as Map objects are immutable
Note: Use .set() method for functional updates instead
"""Usage Examples
# Create maps
map1 = Map({1: 'one', 2: 'two', 3: 'three'})
map2 = Map({3: 'THREE', 4: 'four'})
# Map operations
updated = map1.set(4, 'four') # Add new key-value pair
removed = map1 - [2, 3] # Remove keys
merged = map1 | map2 # Merge (map2 values take precedence)
# Properties
print(map1.keys) # Set({1, 2, 3})
print(map1.values) # Set({'one', 'two', 'three'})
print(map1.items) # Set({(1, 'one'), (2, 'two'), (3, 'three')})
# Access
print(map1[1]) # 'one'
print(1 in map1) # TrueArrays (Array)
Multi-dimensional mutable arrays with Dafny semantics, supporting arbitrary dimensions and efficient element access/modification.
class Array:
def __init__(self, initValue, *dims):
"""
Create multi-dimensional array.
Parameters:
- initValue: Initial value for all elements
- dims: Dimension sizes (integers)
"""
def __dafnystr__(self) -> str:
"""Returns string representation showing array dimensions."""
def length(self, i):
"""
Returns length of dimension i.
Parameters:
- i: Dimension index (0-based)
Returns:
int or None: Length of dimension i, or None if i >= number of dimensions
"""
def __len__(self):
"""Returns length of first dimension."""
def __getitem__(self, key):
"""
Gets element at index/indices.
Parameters:
- key: Single index (int) or iterable of indices for multi-dimensional access
Returns:
Element value or sub-array
"""
def __setitem__(self, key, value):
"""
Sets element at index/indices.
Parameters:
- key: Single index (int) or iterable of indices for multi-dimensional access
- value: New value for element
"""Usage Examples
# 1D array
arr1d = Array(0, 5) # [0, 0, 0, 0, 0]
arr1d[2] = 42
print(arr1d[2]) # 42
print(len(arr1d)) # 5
# 2D array
arr2d = Array('', 3, 4) # 3x4 array of empty strings
arr2d[1, 2] = 'hello'
print(arr2d[1, 2]) # 'hello'
print(arr2d.length(0)) # 3 (rows)
print(arr2d.length(1)) # 4 (columns)
# 3D array
arr3d = Array(0.0, 2, 3, 4) # 2x3x4 array of floats
arr3d[0, 1, 3] = 3.14
print(arr3d[0, 1, 3]) # 3.14Utility Functions
Sequence Creation Without String Inference
def SeqWithoutIsStrInference(__iterable=None):
"""
Creates a Seq without string inference (used when --unicode-char is enabled).
Parameters:
- __iterable: Initial elements (optional)
Returns:
Seq: Sequence with isStr=None
"""Usage Example
# For use with --unicode-char compilation flag
seq = SeqWithoutIsStrInference(['a', 'b', 'c'])
# String inference is disabled, preventing automatic string detectionConcatenation Support (Concat)
Internal concatenation structure used by Seq for efficient lazy concatenation operations. This class defers actual concatenation until elements are accessed.
class Concat:
def __init__(self, l, r):
"""
Creates a concatenation structure for lazy evaluation.
Parameters:
- l: Left sequence or concatenation structure
- r: Right sequence or concatenation structure
"""
def __len__(self):
"""
Returns total length of concatenated structure.
Returns:
int: Sum of lengths of left and right structures
"""
def flatten(self):
"""
Flattens the concatenation structure into a list.
Returns:
list: Flattened elements from the concatenation tree
Note: Uses depth-first traversal to collect all elements
"""Usage Examples
from _dafny import Seq, Concat
# Concat is typically used internally by Seq
seq1 = Seq([1, 2, 3])
seq2 = Seq([4, 5, 6])
# When sequences are concatenated, Concat may be used internally
combined = seq1 + seq2 # May create Concat structure internally
# Access triggers flattening when needed
print(combined.Elements) # [1, 2, 3, 4, 5, 6]
# Direct Concat usage (advanced)
concat_struct = Concat([1, 2], [3, 4])
print(len(concat_struct)) # 4
print(concat_struct.flatten()) # [1, 2, 3, 4]Install with Tessl CLI
npx tessl i tessl/pypi-dafnyruntimepython