Commit e4e2cc81 authored by MARCHE Claude's avatar MARCHE Claude

change explanation for the VC of a whole function (no more "parameter")

parent 68dca709
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/anr-bware/why3/share/why3/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -47,13 +47,13 @@
name="WP_parameter isqrt"
locfile="../isqrt.mlw"
loclnum="11" loccnumb="6" loccnume="11"
expl="parameter isqrt"
expl="VC for isqrt"
sum="64277e54f36ba5a32dedb1a194a25f0d"
proved="true"
expanded="false"
shape="iainfix &lt;=V1V0ainfix &lt;ainfix -V0V3ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4asqrainfix +V3c1Aainfix &gt;=V0asqrV3Aainfix &gt;=V3c0Iainfix =V4ainfix +ainfix +V1ainfix *c2V3c1FIainfix =V3ainfix +V2c1Fainfix &lt;V0asqrainfix +V2c1Aainfix &lt;=asqrV2V0Aainfix &gt;=V2c0Iainfix =V1asqrainfix +V2c1Aainfix &gt;=V0asqrV2Aainfix &gt;=V2c0FAainfix =c1asqrainfix +c0c1Aainfix &gt;=V0asqrc0Aainfix &gt;=c0c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter isqrt"/>
name="expl:VC for isqrt"/>
<proof
prover="2"
timelimit="2"
......@@ -83,13 +83,13 @@
name="WP_parameter main"
locfile="../isqrt.mlw"
loclnum="24" loccnumb="6" loccnume="10"
expl="parameter main"
expl="VC for main"
sum="27febadb619ab97b0f5570efb544d5b3"
proved="true"
expanded="false"
shape="ainfix =V0c4Iainfix &lt;c17asqrainfix +V0c1Aainfix &lt;=asqrV0c17Aainfix &gt;=V0c0FAainfix &gt;=c17c0">
<label
name="expl:parameter main"/>
name="expl:VC for main"/>
<proof
prover="5"
timelimit="2"
......@@ -118,13 +118,13 @@
name="WP_parameter sqrt"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="80ef3a8dd2bff270b44a0e173c090b27"
proved="false"
expanded="true"
shape="iainfix =V0c0ainfix &lt;V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix &lt;=ainfix *c0c0V0iainfix &lt;=V0c3ainfix &lt;V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix &lt;=ainfix *c1c1V0iainfix &lt;V1V2ainfix &lt;V3V2Aainfix &lt;=c0V2Aainfix &lt;V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix &lt;V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix &gt;V3c0Aainfix &gt;V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1Fainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix &lt;=ainfix *V2V2V0Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FAainfix &lt;V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix &lt;V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix &gt;V0c0Aainfix &gt;adivainfix +V0c1c2c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<transf
name="split_goal"
proved="false"
......@@ -139,7 +139,7 @@
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix &lt;=ainfix *c0c0V0Iainfix =V0c0Iainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="20"
......@@ -183,7 +183,7 @@
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix &lt;=ainfix *c1c1V0Iainfix &lt;=V0c3Iainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -227,7 +227,7 @@
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Aainfix &lt;V0ainfix *ainfix +V0c1ainfix +V0c1Aainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Aainfix &gt;V0c0Aainfix &gt;adivainfix +V0c1c2c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<transf
name="split_goal"
proved="true"
......@@ -236,13 +236,13 @@
name="WP_parameter sqrt.3.1"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="24aeef4693626abd3583f6b6921aba3d"
proved="true"
expanded="false"
shape="ainfix &gt;adivainfix +V0c1c2c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -280,13 +280,13 @@
name="WP_parameter sqrt.3.2"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="92c82885df59e2741ce4df823ca7822c"
proved="true"
expanded="false"
shape="ainfix &gt;V0c0Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -324,13 +324,13 @@
name="WP_parameter sqrt.3.3"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="fb51c594670b2b8984a4e1f8acf2af68"
proved="true"
expanded="false"
shape="ainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="2"
timelimit="10"
......@@ -352,13 +352,13 @@
name="WP_parameter sqrt.3.4"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="1f2b528636f5a3179f0d71f5ce38fb47"
proved="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +V0c1ainfix +V0c1Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -396,13 +396,13 @@
name="WP_parameter sqrt.3.5"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="ca389f1cbcafdb15628b4e6e6c6538b1"
proved="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Iainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -448,7 +448,7 @@
expanded="true"
shape="ainfix &lt;V0ainfix *ainfix +V4c1ainfix +V4c1Aainfix &lt;V0ainfix *ainfix +V3c1ainfix +V3c1Aainfix =V4adivainfix +adivV0V3V3c2Aainfix &gt;V3c0Aainfix &gt;V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<transf
name="split_goal"
proved="false"
......@@ -457,13 +457,13 @@
name="WP_parameter sqrt.4.1"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="dbbf6c132fa37dd1bf514c64adea52e1"
proved="true"
expanded="false"
shape="ainfix &gt;V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -501,13 +501,13 @@
name="WP_parameter sqrt.4.2"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="e227034cdab8f00eb1fac96f38ccca97"
proved="true"
expanded="false"
shape="ainfix &gt;V3c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -545,13 +545,13 @@
name="WP_parameter sqrt.4.3"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="c9f4a06133300f4616cdea414a4417a1"
proved="true"
expanded="false"
shape="ainfix =V4adivainfix +adivV0V3V3c2Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -589,13 +589,13 @@
name="WP_parameter sqrt.4.4"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="87a2f741d5f9c56a2e7094f8b716367e"
proved="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +V3c1ainfix +V3c1Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -625,13 +625,13 @@
name="WP_parameter sqrt.4.5"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="parameter sqrt"
expl="VC for sqrt"
sum="4d60792da3a13e5506152f2dbc8e83b6"
proved="false"
expanded="true"
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +V4c1ainfix +V4c1Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="10"
......@@ -709,7 +709,7 @@
expanded="false"
shape="ainfix &lt;V3V2Aainfix &lt;=c0V2Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix &lt;V1V2Iainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="20"
......@@ -753,7 +753,7 @@
expanded="false"
shape="ainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix &lt;=ainfix *V2V2V0Iainfix &lt;V1V2NIainfix &lt;V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix &lt;V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix &gt;V2c0Aainfix &gt;V1c0FIainfix &lt;=V0c3NIainfix =V0c0NIainfix &gt;=V0c0F">
<label
name="expl:parameter sqrt"/>
name="expl:VC for sqrt"/>
<proof
prover="0"
timelimit="20"
......
......@@ -884,7 +884,7 @@ let rec unabsurd f = match f.t_node with
let add_wp_decl km name f uc =
(* prepare a proposition symbol *)
let s = "WP_parameter " ^ name.id_string in
let lab = Ident.create_label ("expl:parameter " ^ name.id_string) in
let lab = Ident.create_label ("expl:VC for " ^ name.id_string) in
let label = Slab.add lab name.id_label in
let id = id_fresh ~label ?loc:name.id_loc s in
let pr = create_prsymbol id in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment