This is what the result should be

sample_contracts.py

@invariant(lambda self: self.value >= 0)
class PositiveInt(object):
  @post(lambda self: self.num_changes == 0 and self.value == 0)
  def __init__(self):
    self.value = 0
    self.num_changes = 0

  @post(lambda new, old: new.num_changes == old.num_changes + 1)
  def add(self, x):
    self.value += x
    if self.value < 0: self.value = 0
    self.num_changes += 1

  @pre(lambda self: self.value < 100) # We don't want to compute big numbers :-)
  def fact(self):
    n = 1
    for i in range(1, self.value+1): n *= i
    return n