Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Pre- and postcondition checker for Python 3

branch: master

Fetching latest commit…

Octocat-spinner-32-eaf2f5

Cannot retrieve the latest commit at this time

Octocat-spinner-32 README.markdown
Octocat-spinner-32 sanity.py
Octocat-spinner-32 usesanity.py
README.markdown

Sanity

from sanity import *

An experimental pre- and postcondition checking library for Python 3.

@sane
def sqrt(x: P > 0):
    import math
    return math.sqrt(x)

print(sqrt(9))
# prints 3.0

print(sqrt(-9))
# ValueError: precondition (-9) > 0 failed
@sane
def square(x) -> P > 0:
    return x * x

print(square(5))
# prints 25

class BadInt(int):
    def __mul__(self, other):
        return -int.__mul__(self, other)

print(square(BadInt(5)))
# ValueError: precondition (-25) > 0 failed

It uses operator overloading and other magic methods to be able to test some pretty advanced conditions.

@sane
def fork(lst: Len(P) % 2 == 0):
    # notice capital letter
    # we can't use len(P) because len() wants to return an int
    # so sanity provides a function Len(t) which simply returns t.__len__()
    return lst[::2], lst[1::2]

print(fork([1, 2, 3, 4]))
# prints ([1, 3], [2, 4])

print(fork([1, 2, 3]))
# ValueError: precondition ((len([1, 2, 3])) % 2) == 0 failed
class Person:
    def __init__(self, parent=None):
        self.parent = parent
    def __repr__(self):
        if self.parent is None:
            return 'someone'
        return 'child of ' + repr(self.parent)
    @sane
    def grandparent(self: P.parent != None):
        return self.parent.parent

print(Person(Person(Person(Person()))).grandparent())
# prints "child of someone"

print(Person().grandparent())
# ValueError: precondition ((someone).parent) != None failed
@sane
def tail(*args: Len(P) > 0):
    return args[1:]

print(tail(10, 11, 12))
# prints (11, 12)
print(tail())
# ValueError: precondition (len(())) > 0 failed
@sane
def pos_sub(a: P > Predicate.b, b):
    # or: Predicate.a > Predicate.b
    return a - b
@sane
def fork(lst: Len(P) % 2 == 0) -> All(Len(P) == 2, Len(P[0]) == Len(P[1])):
    return lst[::2], lst[1::2]

This is currently not possible since the current design only allows one argument for a predicate, which requires all predicates to be a single line, so no multiple Ps per condition.

Something went wrong with that request. Please try again.