###############################################################################
#
# This example shows how preconditions and postconditions are integrated into
# the implementation of methods/functions.
#
###############################################################################
import sys
import array
###############################################################################
# Possible error codes
NORMAL, OVERFLOW, UNDERFLOW, NEGATIVE_SIZE, NOT_INTEGER = range(5)
###############################################################################
class IntegerStack3:
"""
Stacks: Data tructures with a Last-In, First-Out access policy.
This stack holds integer elements.
This is the tolerant version, setting an error code in case of impossible
operations.
"""
# maximum number of stack elements
_capacity = None
# number of stack elements
_count = 0
# error code
_error = NORMAL
# the array used to hold the stack elements
_representation = array.array('i', [])
def __init__(self, n = 0):
"""Allocate stack for a maximum of n elements if n is non-negative int.
post::
# error code is set to NEGATIVE_SIZE if n is negative
implies(n < 0, self.error() is NEGATIVE_SIZE)
# error code is set to NOT_INTEGER if n is not an integer
implies(not isinstance(n, int), self.error() is NOT_INTEGER)
# no error if n is non-negative integer
implies(n >= 0 and isinstance(n, int), self.error() is NORMAL)
# stack compacity is equal to n if no error occurs
implies(self.error() is NORMAL, self.capacity() is n)
# stack is empty if no error occurs
implies(self.error() is NORMAL, self.is_empty())
# representation is allocated if no error occurs
implies(self.error() is NORMAL, self._representation is not None)
"""
if n < 0:
self._error = NEGATIVE_SIZE
elif not isinstance(n, int):
self._error = NOT_INTEGER
else:
self._capacity = n
def capacity(self):
"""Maximum number of stack elements."""
return self._capacity
def count(self):
"""Number of stack elements."""
return self._count
def error(self):
"""Error code."""
return self._error
def item(self):
"""Return top element if stack is not empty.
post[self]::
# no error if stack is not empty
implies(not __old__.self.is_empty(), self.error() is NORMAL)
# set error code to UNDERFLOW if stack is empty
implies(__old__.self.is_empty(), self.error() is UNDERFLOW)
"""
result = None
if self.is_empty():
self._error = UNDERFLOW
else:
result = self._representation[len(self._representation) - 1]
self._error = NORMAL
return result
def is_empty(self):
"""Is stack empty?
post::
# stack is empty if and only if its element count is 0
__return__ == (self._count == 0)
"""
return self.count() == 0
def is_full(self):
"""Is stack representation full?
post::
# stack is full if and only if its element count is equal to
# its capacity
__return__ == (self.count() == self.capacity())
"""
return self.count() == self.capacity()
def put(self, x):
"""Put x on top if stack is not full and x is integer.
post[self]::
# set error code to NOT_INTEGER if x is not integer
implies(not isinstance(x, int), self.error() is NOT_INTEGER)
# set error code to OVERFLOW if stack is full
implies(__old__.self.is_full(), self.error() is OVERFLOW)
# error code is NORMAL if stack is not full and x is integer
implies(isinstance(x, int) and not __old__.self.is_full(),
self.error() is NORMAL)
# stack is not empty if no error occurs
implies(self.error() is NORMAL, not self.is_empty())
# the top element is x if no error occurs
implies(self.error() is NORMAL,
self.capacity() is 0 or
self._representation[len(self._representation) - 1] is x)
# stack element count increases by 1 if no error occurs
implies(self.error() is NORMAL,
self.count() is __old__.self.count() + 1)
"""
if not isinstance(x, int):
self._error = NOT_INTEGER
elif self.is_full():
self._error = OVERFLOW
else:
self._representation.append(x)
self._count += 1
self._error = NORMAL
def remove(self):
"""Remove top element if stack is not empty.
post[self]::
# set error code to UNDERFLOW if stack is empty
implies(__old__.self.is_empty(), self.error() is UNDERFLOW)
# error code is NORMAL is stack is not empty
implies(not __old__.self.is_empty(), self.error() is NORMAL)
# stack is not full if no error occurs
implies(self.error() is NORMAL, not self.is_full())
# stack element count decrease by 1 if no error occurs
implies(self.error() is NORMAL,
self.count() is __old__.self.count() - 1)
"""
if self.is_empty():
self._error = UNDERFLOW
else:
self._representation.pop()
self._count -= 1
self._error = NORMAL
###############################################################################
import contract
contract.checkmod(__name__)
###############################################################################
if __name__ == '__main__':
# a stack able to hold only 1 element
x = IntegerStack3(1)
x.put(1)
print 'Error:', x.error()
x.put(2)
print 'Error:', x.error()
x.remove()
print 'Error:', x.error()
print x.item()
print 'Error:', x.error()
# a stack unable to hold any element
y = IntegerStack3()
y.put(1)
y.put(2)
y.remove()
print y.item()
###############################################################################