use type option from the library

parent 326d87ce
......@@ -2,12 +2,11 @@
module FibMemo
use import option.Option
use import int.Int
use import int.Fibonacci
use import ref.Ref
type option 'a = None | Some 'a
use import map.Map as M
type table = M.map int (option int)
......
......@@ -20,15 +20,15 @@
<theory
name="FibMemo"
locfile="../fib_memo.mlw"
loclnum="3" loccnumb="7" loccnume="8"
loclnum="3" loccnumb="7" loccnume="14"
verified="true"
expanded="true">
<goal
name="WP_parameter fibo"
locfile="../fib_memo.mlw"
loclnum="30" loccnumb="10" loccnume="14"
loclnum="29" loccnumb="10" loccnume="14"
expl="VC for fibo"
sum="a3a8eda4fb2be551467fdd49b1e76c6e"
sum="fecb48e8fc4d7a5c368af18b3ca54644"
proved="true"
expanded="true"
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Aainfix &lt;ainfix +ainfix *c2V4c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Aainfix &lt;ainfix +ainfix *c2V2c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c2ainvV1Aainfix =V0afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
......@@ -46,9 +46,9 @@
<goal
name="WP_parameter memo_fibo"
locfile="../fib_memo.mlw"
loclnum="39" loccnumb="7" loccnume="16"
loclnum="38" loccnumb="7" loccnume="16"
expl="VC for memo_fibo"
sum="3acd9e9482cadd41f279143eec17329d"
sum="e8643d790b31ef3ed015ee955c2b771d"
proved="true"
expanded="true"
shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FAainvV1Aainfix &lt;=c0V0Aainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix &lt;=c0V0FF">
......@@ -61,9 +61,9 @@
<goal
name="WP_parameter memo_fibo.1"
locfile="../fib_memo.mlw"
loclnum="39" loccnumb="7" loccnume="16"
loclnum="38" loccnumb="7" loccnume="16"
expl="1. postcondition"
sum="721b426fbf3f2646870759e3930c9806"
sum="add45f61cf2c2f73b4bb3656a75d1093"
proved="true"
expanded="true"
shape="postconditionainvV1Aainfix =V2afibV0Iainfix =agetV1V0aSomeV2FIainvV1Aainfix &lt;=c0V0FF">
......@@ -81,9 +81,9 @@
<goal
name="WP_parameter memo_fibo.2"
locfile="../fib_memo.mlw"
loclnum="39" loccnumb="7" loccnume="16"
loclnum="38" loccnumb="7" loccnume="16"
expl="2. variant decrease"
sum="1df4dba295e92068f22a2d699f92e0de"
sum="c1b54c2b8a4caa4ed12625b3781be505"
proved="true"
expanded="false"
shape="variant decreaseainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......@@ -101,9 +101,9 @@
<goal
name="WP_parameter memo_fibo.3"
locfile="../fib_memo.mlw"
loclnum="39" loccnumb="7" loccnume="16"
loclnum="38" loccnumb="7" loccnume="16"
expl="3. precondition"
sum="11605f571d7d37e1a881c8932a63c25a"
sum="db263480dd5c3f26d2811f05e4c77980"
proved="true"
expanded="true"
shape="preconditionainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......@@ -121,9 +121,9 @@
<goal
name="WP_parameter memo_fibo.4"
locfile="../fib_memo.mlw"
loclnum="39" loccnumb="7" loccnume="16"
loclnum="38" loccnumb="7" loccnume="16"
expl="4. postcondition"
sum="b904ccf2d4702a4d58f8fd5a49c03549"
sum="7504a485752626786916e0645018ebc8"
proved="true"
expanded="true"
shape="postconditionainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FIainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......
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