tessl/pypi-dafnyruntimepython
Python runtime library for Dafny, providing essential data structures, type representations, and utility functions for executing Dafny-compiled Python code
—
Pending
mathematical-types.mddocs/
Mathematical Types
High-precision mathematical types for arbitrary precision arithmetic and ordinal number operations. These types preserve mathematical accuracy and implement Dafny's mathematical semantics in Python.
Capabilities
Arbitrary Precision Rational Numbers (BigRational)
Extends Python's Fraction class with Dafny-specific decimal formatting and arithmetic operations. Provides exact rational arithmetic without floating-point precision loss.
class BigRational(Fraction):
def __dafnystr__(self):
"""
Returns Dafny-specific string representation with decimal formatting.
Returns:
str: Decimal representation or fraction notation for non-decimal rationals
"""
def is_integer(self):
"""
Tests if the rational number is an integer.
Returns:
bool: True if the rational equals an integer value
"""
def __add__(self, other):
"""
Addition returning BigRational.
Parameters:
- other: Another BigRational, Fraction, or numeric type
Returns:
BigRational: Sum as a BigRational
"""
def __sub__(self, other):
"""
Subtraction returning BigRational.
Parameters:
- other: Another BigRational, Fraction, or numeric type
Returns:
BigRational: Difference as a BigRational
"""
def __mul__(self, other):
"""
Multiplication returning BigRational.
Parameters:
- other: Another BigRational, Fraction, or numeric type
Returns:
BigRational: Product as a BigRational
"""
def __truediv__(self, other):
"""
Division returning BigRational.
Parameters:
- other: Another BigRational, Fraction, or numeric type
Returns:
BigRational: Quotient as a BigRational
"""
@staticmethod
def isolate_factor(f, x):
"""
Factors out powers of f from x.
Parameters:
- f: Factor to isolate
- x: Number to factor
Returns:
tuple: (remaining_factor, exponent)
"""
@staticmethod
def divides_a_power_of_10(x):
"""
Checks if x divides a power of 10 (for decimal representation).
Parameters:
- x: Denominator to check
Returns:
tuple or None: (compensation, shift) if divisible, None otherwise
"""Usage Examples
from _dafny import BigRational
# Create rational numbers
half = BigRational(1, 2) # 1/2
third = BigRational(1, 3) # 1/3
decimal_val = BigRational(25, 100) # 0.25
# Arithmetic operations
sum_val = half + third # 5/6
product = half * decimal_val # 1/8 = 0.125
division = BigRational(7, 3) / BigRational(2, 1) # 7/6
# String representations
print(half.__dafnystr__()) # "0.5"
print(third.__dafnystr__()) # "(1.0 / 3.0)" - non-decimal
print(decimal_val.__dafnystr__()) # "0.25"
# Type checking
print(BigRational(4, 1).is_integer()) # True
print(third.is_integer()) # False
# Exact arithmetic (no floating-point errors)
result = BigRational(1, 10) + BigRational(2, 10) + BigRational(7, 10)
print(result == BigRational(1, 1)) # True (exactly 1.0)Ordinal Numbers (BigOrdinal)
Operations on ordinal numbers. At runtime, all ordinals are represented as natural numbers, but the class provides the conceptual framework for ordinal arithmetic.
class BigOrdinal:
@staticmethod
def is_limit(ord):
"""
Tests if ordinal is a limit ordinal.
Parameters:
- ord: Ordinal number (represented as int at runtime)
Returns:
bool: True if ord is a limit ordinal (currently: ord == 0)
"""
@staticmethod
def is_succ(ord):
"""
Tests if ordinal is a successor ordinal.
Parameters:
- ord: Ordinal number (represented as int at runtime)
Returns:
bool: True if ord is a successor ordinal (currently: ord > 0)
"""
@staticmethod
def offset(ord):
"""
Returns the offset of the ordinal.
Parameters:
- ord: Ordinal number
Returns:
int: The ordinal value itself (at runtime)
"""
@staticmethod
def is_nat(ord):
"""
Tests if ordinal is a natural number.
Parameters:
- ord: Ordinal number
Returns:
bool: Always True (all ordinals are natural numbers at runtime)
"""Usage Examples
from _dafny import BigOrdinal
# Ordinal operations (all ordinals are natural numbers at runtime)
ord_zero = 0
ord_five = 5
# Test ordinal properties
print(BigOrdinal.is_limit(ord_zero)) # True (0 is limit ordinal)
print(BigOrdinal.is_limit(ord_five)) # False
print(BigOrdinal.is_succ(ord_zero)) # False
print(BigOrdinal.is_succ(ord_five)) # True (successor ordinal)
print(BigOrdinal.offset(ord_five)) # 5
print(BigOrdinal.is_nat(ord_five)) # True (always true at runtime)Character Arithmetic
Mathematical operations on Unicode characters, treating them as their numeric code point values.
def plus_char(a, b):
"""
Adds the Unicode code points of two characters.
Parameters:
- a: str - First character
- b: str - Second character
Returns:
str: Character with code point equal to sum of input code points
"""
def minus_char(a, b):
"""
Subtracts the Unicode code point of second character from first.
Parameters:
- a: str - First character
- b: str - Second character
Returns:
str: Character with code point equal to difference of input code points
"""Usage Examples
from _dafny import plus_char, minus_char
# Character arithmetic
result1 = plus_char('A', '\x01') # 'B' (65 + 1 = 66)
result2 = minus_char('Z', '\x01') # 'Y' (90 - 1 = 89)
# Working with numeric offsets
offset = plus_char('a', '\x05') # 'f' (97 + 5 = 102)
back = minus_char(offset, '\x05') # 'a' (back to original)Euclidean Division and Modulus
Mathematical division and modulus operations following Euclidean division rules, ensuring consistent behavior across positive and negative numbers.
def euclidian_division(a, b):
"""
Performs Euclidean division.
Parameters:
- a: int - Dividend
- b: int - Divisor
Returns:
int: Quotient following Euclidean division rules
"""
def euclidian_modulus(a, b):
"""
Performs Euclidean modulus operation.
Parameters:
- a: int - Dividend
- b: int - Divisor
Returns:
int: Non-negative remainder following Euclidean modulus rules
"""Usage Examples
from _dafny import euclidian_division, euclidian_modulus
# Euclidean division (consistent with mathematical definition)
print(euclidian_division(7, 3)) # 2
print(euclidian_division(-7, 3)) # -3
print(euclidian_division(7, -3)) # -2
print(euclidian_division(-7, -3)) # 3
# Euclidean modulus (remainder is always non-negative)
print(euclidian_modulus(7, 3)) # 1
print(euclidian_modulus(-7, 3)) # 2 (not -1)
print(euclidian_modulus(7, -3)) # 1
print(euclidian_modulus(-7, -3)) # 2
# Property: a = (euclidian_division(a, b) * b) + euclidian_modulus(a, b)
a, b = -7, 3
div = euclidian_division(a, b) # -3
mod = euclidian_modulus(a, b) # 2
print(a == div * b + mod) # True: -7 == (-3 * 3) + 2Install with Tessl CLI
npx tessl i tessl/pypi-dafnyruntimepython