Pythonで__CPROVER_assertの効果を得るには？

Question

私はその値val1> = val2をアサートする必要があります。それはモデルチェックの点では、証人（反例）はval1> = val2と主張する必要があります。 Pythonでそれをする方法はあり

C1 = True; 

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

：

私がすることによってC（CBMC）で簡単に行うことができますか？

更新：

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として機能しません。これは、有効/満足の証人/解釈を検出します。

例えば、同じコードの私の3つの異なる実行はと結果：

>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

val1 >= val2がTrueであれば、C1はFalseになり、何AssertionErrorは存在しません、次のPythonコードで（オリジナルのポストを与えられた）：

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

Answer 2

これはあなたが望むものであるならば、私はまだわかりませんあなたがする必要があるが、もしあなたが必要とするすべては2乱数xは、yのように、X> = yのすべての我々は唯一の2つの数字をしたいなどの条件は、この

from random import randint 

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

のように、私たちはビルド - を力を使用することができた場合楽しいction 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とルにそれを渡し、を求めたとしても、できるだけ多くの数を生成するために、generator expressionを使用を使用することができますそれはその仕事をするTと、それは順序が無関係であれば、単純なlist comprehensionが十分

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

例です

ためか

例

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

を下降している場合descendingと私はコントロール

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