### A MODULE/CLASS THAT MODELS A BANK ACCOUNT ###############

# The global variable, the money in the account:
account = 100       # we'll start at 1d0....
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (account == 100)
# the global invariant (sometimes called the _class invariant_):
"""{ globalinvOK  account >= 0  }"""  # this property must stay true forever
#PREMISES FOR NEXT LINE: 
# (account >= 0)

# A real account maintains a log of all the transactions:
log = [0+100]
#PREMISES FOR ATTACHED PROOF, IF ANY: 
# (log == [(0 + 100)])
# (account >= 0)
#PREMISES FOR NEXT LINE: 
# (log == [(0 + 100)])
# (account >= 0)

# There is another global invariant: the  balance  is correct!

### """{ globalinv   account == summation of  i: 0..log(len-1), log[i] }"""

# We can use  def  clauses, explained in Chapter 3, and arrays,
# explained in Chapter 6, to state and prove this property.


def deposit(howmuch) :
    """deposit adds  howmuch  to  account"""
    """{ pre  howmuch >= 0 
         post  True }"""
    global account, log
    #PREMISES FOR NEXT LINE: 
    # (howmuch >= 0)
    # (account >= 0)
    """{ 1.OK  account >= 0    premise # the globalinv holds on entry
         2.OK  howmuch >= 0    premise  # the function's precondition
         3.OK  account >= 0 and howmuch >= 0  andi 1 2
    }"""
    #PREMISES FOR NEXT LINE: 
    # ((account >= 0) and (howmuch >= 0))
    account = account + howmuch
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (account == (account_old + howmuch))
    # ((account_old >= 0) and (howmuch >= 0))
    """{ 1.OK account == account_old + howmuch    premise
         2.OK account_old >= 0  and  howmuch >= 0    premise 
         3.OK account >= 0                         algebra 1 2
    }"""
    #PREMISES FOR NEXT LINE: 
    # (account >= 0)

    log.append(0+howmuch)   # record the transaction in the log
    #PREMISES FOR ATTACHED PROOF, IF ANY: 
    # (log[(len(log) - 1)] == (0 + howmuch))
    # (len(log) == (len(log_old) + 1))
    # (account >= 0)
    #PREMISES FOR NEXT LINE: 
    # (log[(len(log) - 1)] == (0 + howmuch))
    # (account >= 0)
#PREMISES FOR NEXT LINE: 
# (log == [(0 + 100)])
# (account >= 0)

    # We must prove the global invariants are preserved at the exit.


def withdraw(howmuch) :
    """withdraw  removes  howmuch  from  account"""
    """{ pre  howmuch >= 0 
         post  True }""" 
    global account, log
    #PREMISES FOR NEXT LINE: 
    # (howmuch >= 0)
    # (account >= 0)
    # the same premises hold here like in  deposit
    if  howmuch <= account :
        #PREMISES FOR THEN-ARM: 
        # (howmuch <= account)
        # (howmuch >= 0)
        # (account >= 0)
        # now we know that  howmuch <= account :
        account = account - howmuch
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (account == (account_old - howmuch))
        # (howmuch <= account_old)
        # (howmuch >= 0)
        # (account_old >= 0)
        """{ 1.OK account == account_old - howmuch    premise
             2.OK  howmuch <= account_old            premise
             3.OK  account >= 0                     algebra 1 2
        }"""
        #PREMISES FOR NEXT LINE: 
        # (account >= 0)

        log.append(0-howmuch)  # record the transaction in the log
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (log[(len(log) - 1)] == (0 - howmuch))
        # (len(log) == (len(log_old) + 1))
        # (account >= 0)
        #PREMISES FOR NEXT LINE: 
        # (log[(len(log) - 1)] == (0 - howmuch))
        # (account >= 0)

    else :
        #PREMISES FOR ELSE-ARM: 
        # not (howmuch <= account)
        # (howmuch >= 0)
        # (account >= 0)
        """{ 1.OK not(howmuch <= account)     premise
             2.OK  account >= 0               premise  # the invariant
        }"""
        #PREMISES FOR NEXT LINE: 
        # (account >= 0)
        pass
        #PREMISES FOR NEXT LINE: 
        # (account >= 0)
        """{ 1.OK account >= 0                premise }"""
        #PREMISES FOR NEXT LINE: 
        # (account >= 0)
    #PREMISES FOR NEXT LINE: 
    # (account >= 0)
    # (howmuch >= 0)
    # END IF
    """{ 1.OK account >= 0                     premise }"""
    #PREMISES FOR NEXT LINE: 
    # (account >= 0)
#PREMISES FOR NEXT LINE: 
# (log == [(0 + 100)])
# (account >= 0)
    # We reprove the global invariants here.