# Using Python decorators to do Hoare Logic

I'm relatively new to Python from a strong Java background. I am trying to create a base class to do Hoare Logic. Function decorators seem to be the way to go with this. I've produced the following code, can you comment on this, and suggest an easier way to do this? It seems awfully over complicated to how easy this would be with an abstract function in Java. I'm quite liking Python's function points from my C/C++ days, something Java doesn't easily support without introspection.

Hoare Logic

{P} {C} {Q}


Where:

• P is the pre-condition
• C is the command
• Q is the post-condition or invariant.

The python decorator

def hoare_logic(description, pre_execution=None, post_execution=None):
def decorator_func(function_to_decorate):
def wrapper_func(*args, **kwargs):
# Hoare Pre-Condition
if pre_execution is not None:
pre_condition = pre_execution(*args, **kwargs)
print("Hoare Pre-Condition {!r}".format(description, pre_condition))
# Hoare Command
return_value = function_to_decorate(*args, **kwargs)

# Hoare Post-Condition
if post_execution is not None:
post_condition = post_execution(*args, **kwargs)
print("Hoare Post-Condition {!r}".format(description, post_condition))

return return_value

return wrapper_func

return decorator_func


Stubs for the pre & post-conditions

def pre_condition():
return True

def post_condition():
return True


Typical usage I want to perform

This is representative of the code under test in a specific scenario, with the pre & post conditions I'd expect to collect several of these into a BDD behaviour class extending the python unittest.TestCase class, or perhaps my own extension of that.

@hoare_logic(description='description of command', pre_condition, post_condition)
def command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError


These are just stubs for exercising the decorator usage above, this is not the way I will really expect to use this in practice, but it is so you can run this code.

    # self.assertRaises(ValueError, command, None)
command(True)
command(False)
command('foo')
command('bar')
command('foobar')


Once I have a grip with the basic mechanism, I intend to adapt this to provide API contracts & a BDD type scenario functionality framework for behaviour & scenario testing. So please keep this in mind. I'm interested in serious scrutiny of the core functionality implementation of the Hoare logic in python.

I'm unsure of my treatment of *args, **kwargs but from what I can see I need this for Python decorators. Is there a better way to handle parametrisation of the wrapped function?

I've deliberately exclude class wrapper & imports to make this simpler run & follow. The commented stub does work if this a class, but not as a script, not quite sure why.

Ultimately I want to be able to do the following, but didn't include this because it is not complete, so consider it pseudo code of my final objective.

@scenario(narrative='short description', givens=[given_one, given_two], thens=[then_one])
def the_behaviour_under_test(arg):
...


Here is everything together Comments suggested I need to add more code, so the full file, this will run as a stand alone python script.

#!/usr/bin/env python

def hoare_logic(description, pre_execution=None, post_execution=None):
def decorator_func(function_to_decorate):
def wrapper_func(*args, **kwargs):
# Hoare Pre-Condition
if pre_execution is not None:
pre_condition = pre_execution()
print("Hoare Pre-Condition {!r}".format(description, pre_condition))

# Hoare Command
return_value = function_to_decorate(*args, **kwargs)

# Hoare Post-Condition
if post_execution is not None:
post_condition = post_execution()
print("Hoare Post-Condition {!r}".format(description, post_condition))

return return_value

return wrapper_func

return decorator_func

def pre_condition():
return True

def post_condition():
return True

@hoare_logic(description='description of command', pre_execution=pre_condition, post_execution=post_condition)
def command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError

# command()
# self.assertRaises(ValueError, command, None)
command(True)
command(False)
command('foo')
command('bar')
command('foobar')

@hoare_logic(description='command')
def naked_command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError

# naked_command()
# self.assertRaises(ValueError, naked_command, None)
naked_command(True)
naked_command(False)
naked_command('foo')
naked_command('bar')
naked_command('foobar')

@hoare_logic(description='description of command', pre_execution=pre_condition)
def pre_command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError

# pre_command()
# self.assertRaises(ValueError, pre_command, None)
pre_command(True)
pre_command(False)
pre_command('foo')
pre_command('bar')
pre_command('foobar')

@hoare_logic(description='description of command', post_execution=post_condition)
def post_command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError

# naked_command()
# self.assertRaises(ValueError, naked_command, None)
post_command(True)
post_command(False)
post_command('foo')
post_command('bar')
post_command('foobar')

@hoare_logic(description='description of command', pre_execution=pre_condition, post_execution=post_condition)
def post_command(arg):
if arg is not None:
print("command")
if arg == 'foobar':
return False
else:
return True
else:
raise ValueError

# post_command()
# self.assertRaises(ValueError, post_command, None)
post_command(True)
post_command(False)
post_command('foo')
post_command('bar')
post_command('foobar')

• Can you explain in more detail what you are trying to do here? The code in the post appears to be unfinished — there is no actual Hoare logic, just printing of conditions, and the example does not even have any conditions that would need to be printed. It is very hard to review code in this kind of state — we'd rather you made your best effort to get it working before posting here. Nov 30 '18 at 12:35
• I've fixed the indent issue, elaborated the question and posted with the entire file I've been experimenting with at the end, rather than the cut down example. Originally I didn't want to cloud thins by posting too much code. Nov 30 '18 at 13:50

You are ignoring the pre_execution and post_execution return values.

def invariant(lst):
return len(lst) > 0

@hoare_logic("Invariants", invariant, invariant)
def append_hello(lst):
"""Append 'hello' to a non-empty list"""

lst.append("Hello")

lst = []
append_hello(lst)


Hoare Pre-Condition 'Invariants'
Hoare Post-Condition 'Invariants'

Neither the False nor the True returned by invariant is used or printed. This comes from your print statement, which only has 1 format code {!r}, but two values are being passed to format().

print("Hoare Pre-Condition {!r}".format(description, pre_condition))


You should either usefully use the pre_condition and post_condition return values, or the pre_execution and post_execution should not be expected to return values, and should raise an exception to indicate a failure of the pre/post conditions.

Your @hoare_logic decorator will hide any """docstring""" which is added to functions:

help(append_hello)


ends up describing the wrapper_func instead of append_hello!

Help on function wrapper_func in module __main__:

wrapper_func(*args, **kwargs)


You should use @functools.wraps to transfer the __name__, docstring, signature, argument type hints, etc from the wrapped function to the wrapping function. After decorating the wrapper ...

import functools

def hoare_logic(description, pre_execution=None, post_execution=None):
def decorator_func(function_to_decorate):
@functools.wraps(function_to_decorate)      # <-- new
def wrapper_func(*args, **kwargs):
# ... body omitted for brevity ...
return wrapper_func
return decorator_func


... then help(append_hello) produces the expected result:

Help on function append_hello in module __main__:

append_hello(lst)
Append 'hello' to a non-empty list