Commit 3b6e790c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

minor fix

parent 16725285
......@@ -42,7 +42,7 @@ module Hanoi
ensures { b.rod = prepend n (old b.rod) }
ensures { c.rod = old c.rod }
= if n > 0 then begin
let ghost t = prepend 0 c.rod in
let ghost t = c.rod in
hanoi_rec a c b (n-1) (Cons n s);
move a b n s;
hanoi_rec c b a (n-1) t
......
......@@ -56,10 +56,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="VC for hanoi_rec"
sum="9ab8b63a5562cfbfc8cbbd55083df18b"
sum="c150d1d30ea2393b5aa8e35087a60e62"
proved="true"
expanded="true"
shape="iainfix >V0c0ainfix =V10V2Aainfix =V11aprependV0V3Aainfix =V12V1AasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10aprependc0V2AasortedV11AasortedV10FACV9aNiltaConsVwainfix >V13ainfix -V0c1ACV8aNiltaConsVwainfix >V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1aprependc0V2Aainfix <ainfix -V0c1V0Aainfix <=c0V0Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FACV6aNiltaConsVwainfix >V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FACV3aNiltaConsVwainfix >V16ainfix -V0c1ACV2aNiltaConsVwainfix >V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Aainfix <ainfix -V0c1V0Aainfix <=c0V0ainfix =V2V2Aainfix =V3aprependV0V3Aainfix =V4V1ICV2aNiltaConsVwainfix >V18V0ACV3aNiltaConsVwainfix >V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="iainfix >V0c0ainfix =V10V2Aainfix =V11aprependV0V3Aainfix =V12V1AasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10V2AasortedV11AasortedV10FACV9aNiltaConsVwainfix >V13ainfix -V0c1ACV8aNiltaConsVwainfix >V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1V2Aainfix <ainfix -V0c1V0Aainfix <=c0V0Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FACV6aNiltaConsVwainfix >V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FACV3aNiltaConsVwainfix >V16ainfix -V0c1ACV2aNiltaConsVwainfix >V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Aainfix <ainfix -V0c1V0Aainfix <=c0V0ainfix =V2V2Aainfix =V3aprependV0V3Aainfix =V4V1ICV2aNiltaConsVwainfix >V18V0ACV3aNiltaConsVwainfix >V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<transf
......@@ -231,10 +231,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="9. precondition"
sum="9050a7d9450a9efe51e9fdc21769a01f"
sum="a42e36f9b07d8a8bde8789fffcafabb8"
proved="true"
expanded="false"
shape="ainfix =V5aprependainfix -V0c1aprependc0V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V10V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V11ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V12ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V13V0ACV3aNiltaConsVwainfix &gt;V14V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="ainfix =V5aprependainfix -V0c1V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V10V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V11ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V12ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V13V0ACV3aNiltaConsVwainfix &gt;V14V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -307,10 +307,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="12. type invariant"
sum="e6003f5dfc8efd1041ac98261260ce7f"
sum="154da48dcf9545287324a9a7c3287270"
proved="true"
expanded="false"
shape="asortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10aprependc0V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1aprependc0V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="asortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -327,10 +327,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="13. postcondition"
sum="a0b54616bb57891714ed9a82ed2e5b08"
sum="8f2f23cf409bc84d65b6c2757a38c168"
proved="true"
expanded="false"
shape="ainfix =V12V1IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10aprependc0V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1aprependc0V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="ainfix =V12V1IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -347,10 +347,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="14. postcondition"
sum="7de79da7c05446aca438a5638b3a595f"
sum="a10a8f942b1651449af069b2c6fc4971"
proved="true"
expanded="false"
shape="ainfix =V11aprependV0V3IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10aprependc0V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1aprependc0V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="ainfix =V11aprependV0V3IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -367,10 +367,10 @@
locfile="../tower_of_hanoi.mlw"
loclnum="36" loccnumb="10" loccnume="19"
expl="15. postcondition"
sum="fa188dbbc9ecec249652dd70f13bd3b7"
sum="1ecd1f3bbbe68f6dbdb64da2be9d658a"
proved="true"
expanded="false"
shape="ainfix =V10V2IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10aprependc0V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1aprependc0V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
shape="ainfix =V10V2IasortedV12Iainfix =V12V9Aainfix =V11aprependainfix -V0c1V8Aainfix =V10V2AasortedV11AasortedV10FICV9aNiltaConsVwainfix &gt;V13ainfix -V0c1ACV8aNiltaConsVwainfix &gt;V14ainfix -V0c1Aainfix =V5aprependainfix -V0c1V2Iainfix =V8aConsV0V6Aainfix =V9V1AasortedV8AasortedV9FICV6aNiltaConsVwainfix &gt;V15V0Aainfix =V7aConsV0V1AasortedV6Iainfix =V6V3Aainfix =V5aprependainfix -V0c1V2Aainfix =V7aConsV0V1AasortedV5AasortedV7FICV3aNiltaConsVwainfix &gt;V16ainfix -V0c1ACV2aNiltaConsVwainfix &gt;V17ainfix -V0c1Aainfix =V4aprependainfix -V0c1aConsV0V1Iainfix &gt;V0c0ICV2aNiltaConsVwainfix &gt;V18V0ACV3aNiltaConsVwainfix &gt;V19V0Aainfix =V4aprependV0V1AasortedV2AasortedV3AasortedV4FF">
<label
name="expl:VC for hanoi_rec"/>
<proof
......@@ -379,7 +379,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......
......@@ -940,8 +940,8 @@ let rec expr_subst psm e = e_label_copy e (match e.e_node with
e_app_real (expr_subst psm e) pv
| Elet ({ let_sym = LetV pv ; let_expr = d }, e) ->
let nd = expr_subst psm d in
let vtv = match nd.e_vty with VTvalue vtv -> vtv | _ -> assert false in
if not (vtv_equal vtv pv.pv_vtv) then Loc.errorm "vty_value mismatch";
if not (vtv_equal (vtv_unmut (vtv_of_expr nd)) pv.pv_vtv) then
Loc.errorm "vty_value mismatch";
e_let { let_sym = LetV pv ; let_expr = nd } (expr_subst psm e)
| Elet ({ let_sym = LetA ps ; let_expr = d }, e) ->
let ld = create_let_defn (id_clone ps.ps_name) (expr_subst psm d) 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