"""
	Simple functions to let us declare pre- and post-conditions
	and make various other logical statements in Python programs.

	Written Summer 2006 by Dave Wonnacott (davew@cs.haverford.edu)

	These all turn into various kinds of exceptions if they ever
	get a "False" value.

	They are currently _very_ primitive, and

	  * The postcondition must be stated just before _each_ return
	  * There is no actual checking of progress

	I hope some day to know enough about Python to make it better...
"""



class LogicConsistencyException(Exception):
	""" Could add more here, if it were needed. """

class PreconditionException(LogicConsistencyException):
	""" Nothing """

class PostconditionException(LogicConsistencyException):
	""" Nothing """

class AssertionException(LogicConsistencyException):
	""" Nothing """

class ProgressException(LogicConsistencyException):
	""" Nothing """

class LoopPreconditionException(LogicConsistencyException):
	""" Nothing """

class LoopPostconditionException(LogicConsistencyException):
	""" Nothing """

class LoopInvariantException(LogicConsistencyException):
	""" Nothing """

class LoopProgressException(LogicConsistencyException):
	""" Nothing """


def precondition(value_of_precondition):
	if (value_of_precondition != True):
		raise PreconditionException

def postcondition(value_of_postcondition):
	if (value_of_postcondition != True):
		raise PostconditionException

def assertion(value_of_assertion):
	if (value_of_assertion != True):
		raise AssertionException

def progress(progress_value):
	if progress_value <= 0 or False:  # still need to check actual progress
		raise ProgessException


def loop_precondition(value_of_loop_precondition):
	if value_of_loop_precondition != True:
		raise LoopPreconditionException

def loop_postcondition(value_of_loop_postcondition):
	if value_of_loop_postcondition != True:
		raise LoopPostconditionException

def loop_invariant(value_of_loop_invariant):
	if value_of_loop_invariant != True:
		raise LoopInvariantException

def loop_progress(loop_progress_value):
	if loop_progress_value < 0 or False:  # still need to check actual progress
		raise LoopProgressException