Skip to content

why3
why3
Commit 74f28874 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

More on io.mlw

parent c67a3b49
Hide whitespace changes
Inline Side-by-side
Showing with 132 additions and 10 deletions
examples/euler001.mlw
View file @ 74f28874
......@@ -188,8 +188,11 @@ module Euler001
use import string.Char
use import io.StdIO
use import ref.Ref
let go () =
let go ()
ensures { !cur_linenum = (old !cur_linenum) + 1 }
=
print_char (chr 71); (* G *)
print_char (chr 79); (* O *)
print_char (chr 58); (* : *)
......
examples/euler001/why3session.xml
View file @ 74f28874
......@@ -984,7 +984,7 @@
locfile="../euler001.mlw"
loclnum="163" loccnumb="6" loccnume="11"
expl="VC for solve"
sum="53c23f7f6496b3723c58106224ec6ea1"
sum="200296912b5b99c365d044e031f76312"
proved="true"
expanded="false"
shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3V1ainfix +V1c1ainfix *ainfix *c5V2ainfix +V2c1ainfix *ainfix *c15V3ainfix +V3c1c2asum_multiple_3_5_ltV0Ladivainfix -V0c1c15Ladivainfix -V0c1c5Ladivainfix -V0c1c3Iainfix >=V0c1F">
......@@ -1028,7 +1028,7 @@
locfile="../euler001.mlw"
loclnum="176" loccnumb="6" loccnume="9"
expl="VC for run"
sum="d23ff9ccc58983c27e6aa9eee7a9f1af"
sum="284d1b9e6d12920da46e6f6c54a8037f"
proved="true"
expanded="false"
shape="ainfix >=c1000c1">
......@@ -1048,7 +1048,7 @@
locfile="../euler001.mlw"
loclnum="182" loccnumb="6" loccnume="11"
expl="VC for bench"
sum="0dcae62fb187df85b26250a70b69538d"
sum="5dada1ffeee7c305d1541d7f4093abcd"
proved="true"
expanded="false"
shape="t">
......@@ -1066,18 +1066,118 @@
<goal
name="WP_parameter go"
locfile="../euler001.mlw"
loclnum="191" loccnumb="6" loccnume="8"
loclnum="193" loccnumb="6" loccnume="8"
expl="VC for go"
sum="fbc052aded7f685e7674843a291fd493"
sum="0ac8af78cda25414bc3f614bbe49b1cf"
proved="true"
expanded="false"
shape="t">
shape="ainfix =V12ainfix +V0c1Iainfix =V15aConsareverseV11V3Aainfix =V12ainfix +V0c1Aainfix =V14aNilAainfix =V13c0FIainfix =V11aConsaPrCharamk charc32V9Aainfix =V10ainfix +V8c1FAainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FAainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FAainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FAainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="WP_parameter go.1"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="1. precondition"
sum="f4b435e3c7c416c20c0ceacb2df6b3c7"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter go.2"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="2. precondition"
sum="abd8cc3f32089b628b51946de8e1f545"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.3"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="3. precondition"
sum="52fac0728ac3d37e1cf005143aeda71d"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.4"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="4. precondition"
sum="b862795097c52804b1f9c8df726d5eb4"
proved="true"
expanded="false"
shape="preconditionainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FIainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter go.5"
locfile="../euler001.mlw"
loclnum="193" loccnumb="6" loccnume="8"
expl="5. postcondition"
sum="ddceb58388c30c795f01682eeffde5dc"
proved="true"
expanded="false"
shape="postconditionainfix =V12ainfix +V0c1Iainfix =V15aConsareverseV11V3Aainfix =V12ainfix +V0c1Aainfix =V14aNilAainfix =V13c0FIainfix =V11aConsaPrCharamk charc32V9Aainfix =V10ainfix +V8c1FIainfix &lt;=c32c255Aainfix &lt;=c0c32Iainfix =V9aConsaPrCharamk charc58V7Aainfix =V8ainfix +V6c1FIainfix &lt;=c58c255Aainfix &lt;=c0c58Iainfix =V7aConsaPrCharamk charc79V5Aainfix =V6ainfix +V4c1FIainfix &lt;=c79c255Aainfix &lt;=c0c79Iainfix =V5aConsaPrCharamk charc71V2Aainfix =V4ainfix +V1c1FIainfix &lt;=c71c255Aainfix &lt;=c0c71F">
<label
name="expl:VC for go"/>
<proof
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
</theory>
......
modules/io.mlw
View file @ 74f28874
......@@ -4,10 +4,24 @@ module StdIO
use import string.Char
(*i use import string.String *)
(*i TODO: add a ghost reference to represent the standard output *)
(** ghost references to represent the standard output *)
use import int.Int
use import list.List
use list.Reverse
use import ref.Ref
type prdata = PrChar char | PrInt int
val flushed : ref (list (list prdata))
val current_line : ref (list prdata)
val cur_pos : ref int
val cur_linenum: ref int
val print_char (c:char) : unit
(** prints a character on standard output. *)
val print_char (c:char) : unit
writes { cur_pos, current_line }
ensures { !cur_pos = (old !cur_pos) + 1 }
ensures { !current_line = Cons (PrChar c) (old !current_line) }
(*i val print_string (s:string) : unit *)
(*i prints a string on standard output. *)
......@@ -21,8 +35,13 @@ val print_int (n: int) : unit
(*i val print_endline (s:string) : unit *)
(*i prints a string, followed by a newline character, on standard output and flushes standard output. *)
val print_newline (u:unit) : unit
(** prints a newline character on standard output, and flushes standard output. *)
val print_newline (u:unit) : unit
writes { cur_pos, current_line, cur_linenum, flushed }
ensures { !cur_pos = 0 }
ensures { !current_line = Nil }
ensures { !cur_linenum = (old !cur_linenum) + 1 }
ensures { !flushed = Cons (Reverse.reverse (old !current_line)) (old !flushed) }
end
......
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