or run

npx @tessl/cli init
Log in

Version

Tile

Overview

Evals

Files

docs

control-flow.mddata-structures.mdindex.mdmathematical-types.mdsystem-types.mdutilities.md
tile.json

tessl/pypi-dafnyruntimepython

Python runtime library for Dafny, providing essential data structures, type representations, and utility functions for executing Dafny-compiled Python code

Workspace
tessl
Visibility
Public
Created
Last updated
Describes
pypipkg:pypi/dafnyruntimepython@4.10.x

To install, run

npx @tessl/cli install tessl/pypi-dafnyruntimepython@4.10.0

index.mddocs/

DafnyRuntimePython

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.

Package Information

  • Package Name: DafnyRuntimePython
  • Language: Python
  • Installation: pip install DafnyRuntimePython
  • Minimum Python Version: 3.8+

Core Imports

import _dafny
from _dafny import Seq, Set, MultiSet, Map, Array, BigRational

For System module types:

import System_
from System_ import nat

Basic Usage

import _dafny
from _dafny import Seq, Set, Map, BigRational

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

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

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

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

# String conversion with Dafny semantics
print(_dafny.string_of(seq))  # [1, 2, 3, 4, 5]
print(_dafny.string_of(string_seq))  # hello

Architecture

The runtime library consists of two main modules:

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

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.

Capabilities

Core Data Structures

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.

class Seq:
    def __init__(self, iterable=None, isStr=False): ...
    def __add__(self, other): ...
    def __getitem__(self, key): ...
    def set(self, key, value): ...

class Set(frozenset):
    def union(self, other): ...
    def intersection(self, other): ...
    def ispropersubset(self, other): ...

class MultiSet(Counter):
    def union(self, other): ...
    def intersection(self, other): ...
    
class Map(dict):
    def set(self, key, value): ...
    def __or__(self, other): ...

class Array:
    def __init__(self, initValue, *dims): ...
    def length(self, i): ...

Core Data Structures

Mathematical Types

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

class BigRational(Fraction):
    def __dafnystr__(self): ...
    def is_integer(self): ...
    def __add__(self, other): ...
    def __truediv__(self, other): ...

class BigOrdinal:
    @staticmethod
    def is_limit(ord): ...
    @staticmethod
    def is_succ(ord): ...
    @staticmethod
    def is_nat(ord): ...

Mathematical Types

Control Flow and Exceptions

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.

class Break(Exception):
    target: str

class Continue(Exception):
    target: str

class TailCall(Exception): pass

class HaltException(Exception):
    message: str

def label(name: str = None): ...
def c_label(name: str = None): ...

Control Flow

Utility Functions

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

def string_of(value) -> str: ...
def string_from_utf_16(utf_16_code_units): ...
def plus_char(a, b): ...
def minus_char(a, b): ...
def euclidian_division(a, b): ...
def euclidian_modulus(a, b): ...
def quantifier(vals, frall, pred): ...
def AllBooleans(): ...
def AllIntegers(): ...
def IntegerRange(lo, hi): ...

Utility Functions

System Types

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

class nat:
    @staticmethod
    def default(): ...
    @staticmethod
    def _Is(source__): ...

System Types

Types

Core Types

class CodePoint(str):
    escapes: dict
    def __escaped__(self): ...
    def __dafnystr__(self): ...
    @staticmethod
    def is_code_point(i): ...

class Doubler:
    def __init__(self, start): ...
    def __iter__(self): ...

class defaults:
    @staticmethod
    def bool(): ...
    @staticmethod
    def char(): ...
    @staticmethod
    def int(): ...
    @staticmethod
    def real(): ...

class classproperty(property):
    def __get__(self, instance, owner): ...