包含非输入参数变量的PyContract后置条件

Question

希望这将是我在本系列文章中的最后一个问题（我的项目即将结束，除非需求发生变化）。在

我正在为使用PyContract（不是PyContracts）的类方法编写一些约束。在我的一个函数中，我有一个不变量。但是，并不是所有构成后置条件的变量都是函数的输入参数；有些变量是函数本身作用域的局部变量（循环计数器等）。我如何/如何在合同的后置条件条款中捕捉到它们？在

以下是我一直在使用的代码：

def foo(*args, **kwargs):
    """
        pre:
            # some preconditions
        inv:
            # something that's clearly false
            1 == 2
        post:
            g < arg5
    """

    arg1 = kwargs['arg1']
    arg2 = kwargs['arg2']
    arg3 = kwargs['arg3']
    arg4 = kwargs['arg4']
    arg5 = kwargs['arg5']

    g = 0
    while g < arg5:
        vars = generate_data(arg1)
        best = max(arg2(var)for var in vars)
        if best >= arg3:
            return best
        # do stuff
        g += 1

当PyContract告诉我它不知道名称g和{}时，问题就出现了。我把契约中的arg5改为{}，但是PyContract仍然不知道g是什么。我怎样才能解决这个问题？在

我得到的错误是：

^{pr2}$

将g添加到后置条件声明中也没有帮助：

post[kwargs, g]:

此外，有趣的是，用于不变检查的代码似乎根本没有运行

Answer 1

后置条件是在函数完成运行后运行的，这意味着包含函数局部变量（例如arg5和g）的堆栈框架不再在作用域内。在

不过，对于实现契约的库来说，这并不奇怪：关键是在函数应该实现的接口上声明约束，而您似乎希望检查函数的内部状态，而在返回值中不可见。在

您可以通过两种方式前进：

1. 使函数返回要与合同一起检查的状态。如果内部状态不是函数接口的一部分，那么这可能不合适。

2. 使用PyContracts以外的东西来强制约束，例如assert语句，或者在循环之后使用raise AssertionError("while loop should have returned early")语句。