Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
fe8cd6a9
Commit
fe8cd6a9
authored
May 27, 2011
by
MARCHE Claude
Browse files
updated proofs of programs/my_cosine
parent
26fa44ed
Changes
2
Hide whitespace changes
Inline
Side-by-side
examples/my_cosine/why3session.xml
View file @
fe8cd6a9
...
...
@@ -17,16 +17,16 @@
<proof
prover=
"alt-ergo"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.81"
/>
</proof>
<proof
prover=
"
gappa
"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"
unknown
"
time=
"
0
.0
1
"
/>
<proof
prover=
"
z3
"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"
timeout
"
time=
"
2
.0
8
"
/>
</proof>
</goal>
<goal
name=
"TotalError"
sum=
"0851711761327bfdfc8ed8a6b0c1fa03"
proved=
"false"
expanded=
"true"
>
<proof
prover=
"alt-ergo"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"timeout"
time=
"2.0
8
"
/>
<result
status=
"timeout"
time=
"2.0
9
"
/>
</proof>
<proof
prover=
"
gappa
"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"
unknown
"
time=
"
0.01
"
/>
<proof
prover=
"
z3
"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"
timeout
"
time=
"
2.69
"
/>
</proof>
</goal>
</theory>
...
...
examples/programs/my_cosine/why3session.xml
View file @
fe8cd6a9
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name=
"examples/programs/my_cosine/why3session.xml"
>
<file
name=
"../my_cosine.mlw"
verified=
"
fals
e"
expanded=
"true"
>
<theory
name=
"M"
verified=
"
fals
e"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine"
expl=
"correctness of parameter my_cosine"
sum=
"
f89fdf11644955925594e36ac13fca80
"
proved=
"
fals
e"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"
fals
e"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.1"
expl=
"assertion"
sum=
"
e5882e289db8c6ba752b0197911cfa23
"
proved=
"true"
expanded=
"true"
>
<file
name=
"../my_cosine.mlw"
verified=
"
tru
e"
expanded=
"true"
>
<theory
name=
"M"
verified=
"
tru
e"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine"
expl=
"correctness of parameter my_cosine"
sum=
"
dd173c4f589edbafa4fba6e5a9ea3037
"
proved=
"
tru
e"
expanded=
"true"
>
<transf
name=
"split_goal"
proved=
"
tru
e"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.1"
expl=
"assertion"
sum=
"
42f9206597da619fa67e4871bf991914
"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"coq"
timelimit=
"2"
edited=
"my_cosine.mlw_M_WP_parameter my_cosine_1.v"
obsolete=
"false"
>
<result
status=
"valid"
time=
"
3.63
"
/>
<result
status=
"valid"
time=
"
4.07
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter my_cosine.2"
expl=
"precondition"
sum=
"
835240929a7ed987a4162d95e5c84f6a
"
proved=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.2"
expl=
"precondition"
sum=
"
521f9e1a4746ed279e562cb96fa07308
"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"gappa"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter my_cosine.3"
expl=
"precondition"
sum=
"
e76b668f84980d8e838e3a29329b0078
"
proved=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.3"
expl=
"precondition"
sum=
"
504e7961442987cb0289d90730d34b73
"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"gappa"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter my_cosine.4"
expl=
"precondition"
sum=
"
4a7ffc5f36f6cb1ee98787dec2d021cb
"
proved=
"true"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.4"
expl=
"precondition"
sum=
"
1d5279a01c0ab5106801f0d505c8da66
"
proved=
"true"
expanded=
"true"
>
<proof
prover=
"gappa"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
name=
"WP_parameter my_cosine.5"
expl=
"normal postcondition"
sum=
"
ede46e25abe361f5d69fd104ad839c4
c"
proved=
"
fals
e"
expanded=
"true"
>
<goal
name=
"WP_parameter my_cosine.5"
expl=
"normal postcondition"
sum=
"
13c0f34f28d335d948bc64dff073925
c"
proved=
"
tru
e"
expanded=
"true"
>
<proof
prover=
"gappa"
timelimit=
"2"
edited=
""
obsolete=
"false"
>
<result
status=
"
unknown
"
time=
"0.0
0
"
/>
<result
status=
"
valid
"
time=
"0.0
2
"
/>
</proof>
</goal>
</transf>
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment