c-在Python中获得__CPROVER_assert的效果

Question

我必须断言值val1>=val2。也就是说，在模型检查方面，见证人（反例）必须断言val1>=val2。

我可以通过以下方式在C（cbmc）中轻松完成：

C1 = True;
C1 = (C1 && (val1 >= val2));
__CPROVER_assert(!C1 ,"constraint sat");

在Python中有办法做到这一点吗？

更新：

C1  = True
C1 = C1 && (val1 >= val2)
assert not C1 

导致

 File "python_version.py", line 123, in main
    assert not  C1
AssertionError

但如果我做

C1  = True
C1 = C1 && (val1 >= val2)
assert C1

结果与我想要的相反（我想要val2>=val1）。编辑：

import math 
from random import randint
def main():
C1 = True
z = randint(1,10)
r = randint(1,10)
x  = z + 2
y  = r + 2
C1 = C1 and (x >= y)
assert  C1
print(x)
print(y)

根据选择的z和r的值，这将打破或通过并打印x，y。因此，这不像__CPROVER_assert那样工作，它会找到有效/满意的证人/解释！

例如，我对同一代码进行了三次不同的运行，结果是：

>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 
Traceback (most recent call last):
  File "checkPython.py", line 23, in <module>
    main()
  File "checkPython.py", line 15, in main
    assert  C1
AssertionError
>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 
7
4
>mokambo 11:16 PM ~/cost-allocation/Constraint_solving python checkPython.py 
12
11

有没有任何方法可以检查Python中约束的可满足性。

Answer 1

（给定原始帖子）使用以下Python代码，如果val1 >= val2是True，则C1将是False，并且不会有AssertionError:

C1 = True
C1 = C1 ^ (val1 >= val2)
assert not C1

Answer 2

我仍然不确定这是否是你想要的，但如果你只需要2个随机数x，y，这样x>=y，如果强制满足这个条件，你需要做的就是这个

from random import randint
def myRandomTuple(ini,fin):
    x = randint(ini,fin)
    y = randint(ini,fin)
    return (max(x,y),min(x,y))

由于我们只想要两个数字，我们可以使用内置函数max和min来选择这些数字的顺序

使用示例：

>>> myRandomTuple(1,10)
(10, 2)
>>> myRandomTuple(1,10)
(9, 3)
>>> myRandomTuple(1,10)
(7, 1)
>>> myRandomTuple(1,10)
(4, 4)
>>> myRandomTuple(1,10)
(10, 3)
>>> myRandomTuple(1,10)
(8, 1)
>>> x,y = myRandomTuple(1,10)
>>> x
10
>>> y
6

它可以通过返回一个列表来扩展到任意大小，如果我们想对该列表进行排序，我们可以使用内置的sorted函数

def myRandomList(ini,fin,size,descending=True):
    return sorted( (randint(ini,fin) for _ in range(size)), reverse=descending)

在这里，我使用一个生成器表达式，生成所需的任意数量，将其传递给sorted并让它完成自己的工作，使用descending我控制它是降序还是非

示例

>>> myRandomList(1,10,5)
[6, 6, 5, 4, 2]
>>>

如果顺序不相关，那么一个简单的列表理解就足够了

def myRandomList(ini,fin,size):
    return [ randint(ini,fin) for _ in range(size) ]

示例

>>> myRandomList(1,10,5)
[6, 7, 5, 8, 1]
>>>