From c0c3fbf255ca0be1af7b4eee7bd224b39738bd48 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 18 Jun 2020 10:50:12 +0200
Subject: [PATCH] new script for wp_gallery/binary-multiplication
---
...ication_loop_invariant_inv1_ok_preserved.json | 16 ++++++++++++++++
.../binary-multiplication.res.oracle | 9 +++++----
2 files changed, 21 insertions(+), 4 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
new file mode 100644
index 00000000000..a44e4f7a5cf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -0,0 +1,16 @@
+[ { "header": "Range", "tactic": "Wp.range",
+ "params": { "inf": 0, "sup": 1 },
+ "select": { "select": "inside-step", "at": 17, "kind": "have",
+ "occur": 0, "target": "b_3 mod 2", "pattern": "%$b2" },
+ "children": { "Lower 0": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0637,
+ "steps": 96 } ],
+ "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0813,
+ "steps": 120 } ],
+ "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.3008,
+ "steps": 284 } ],
+ "Upper 1": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0965,
+ "steps": 99 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 42a2b002096..92bfb254ae4 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -10,7 +10,6 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
@@ -21,13 +20,15 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 16 / 17
+[wp] [Script] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
+[wp] Proved goals: 17 / 17
Qed: 4
- Alt-Ergo: 12 (unsuccess: 1)
+ Script: 1
+ Alt-Ergo: 12
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 3 9 13 92.3%
+ BinaryMultiplication 3 9 13 100%
------------------------------------------------------------
--
GitLab