Commit 87fa0578 authored by Sylvain Dailler's avatar Sylvain Dailler

Update example of issue 116

parent fa8c97b5
...@@ -4,12 +4,14 @@ module Test ...@@ -4,12 +4,14 @@ module Test
use mach.array.Array63 use mach.array.Array63
constant d: Array.array int constant d: Array.array int
constant e: Array63.array int val e: Array63.array int
(* goal a: e[1] = 5*) goal a: d[1] = 5
goal c: Array.([]) d 3 = 5 let f i =
e[i] <- 5;
e[i]
(* goal g: Array63.([]) e 3 = 5 *) goal c: d[3] = 5
end end
...@@ -2,8 +2,12 @@ ...@@ -2,8 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="5">
<file name="../116_array_access.mlw" proved="true"> <file name="../116_array_access.mlw">
<theory name="Test"> <theory name="Test">
<goal name="a">
</goal>
<goal name="VC f" expl="VC for f">
</goal>
<goal name="c"> <goal name="c">
</goal> </goal>
</theory> </theory>
......
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