1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
from imandra.u.agents import get_remote_graph, create_thread_sync
from imandra.u.agents.code_logician_formalizer import InputState as FInput
from imandra.u.agents.code_logician_reasoner import InputState as RInput, ReasonerAction
# Convert Python code to IML code
code_logician_formalizer = get_remote_graph(agent_name='code_logician_python')
# verify that the result of g(x) is always larger than 0
create_thread_sync(code_logician_formalizer)
src_code = """
def g(x: int):
if x > 22:
return 9
else:
return 100 + x
"""
res = code_logician_formalizer.invoke(FInput(src_lang='python', src_code=src_code))
print(res['end_result']['result'])
# 'success'
iml_code = res['formalizations'][-1]['iml_code']
print(iml_code)
# --------------------------
# let g (x : int) : int =
# if x > 22 then
# 9
# else
# 100 + x
# --------------------------
# Verify some property about the code, or find a counter-example if the property does not hold.
code_logician_reasoner = get_remote_graph(agent_name='code_logician_reasoner')
create_thread_sync(code_logician_reasoner)
res = code_logician_reasoner.invoke(
RInput(
src_code=src_code,
iml_code=iml_code,
action=ReasonerAction(type="extract_verify_reqs"),
)
)
create_thread_sync(code_logician_reasoner)
res = code_logician_reasoner.invoke(
RInput(
src_code=src_code,
iml_code=iml_code,
verify_req=res["verify_req"],
action=ReasonerAction(type="run_verify"),
)
)
print(res['verify_req'][0]['extra']['instance_res']['sat']['model']['src'])
# --------------------------
# module M = struct
#
# let x = (-100.0)
#
# end
# --------------------------
