io.mlw 1.44 KB
Newer Older
1 2
module StdIO

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
3 4
  use import string.Char
  (*i use import string.String *)
5

6 7 8 9 10
  (** ghost references to represent the standard output *)
  use import int.Int
  use import list.List
  use list.Reverse
  use import ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
11

12
  type prdata = PrChar char | PrInt int
MARCHE Claude's avatar
MARCHE Claude committed
13

14 15 16 17
  val ghost flushed : ref (list (list prdata))
  val ghost current_line : ref (list prdata)
  val ghost cur_pos : ref int
  val ghost cur_linenum: ref int
18

19 20 21 22 23
  (** 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) }
24

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
25 26
  (*i val print_string (s:string) : unit *)
  (*i prints a string on standard output. *)
27

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
28 29
  val print_int (n: int) : unit
  (** prints an integer, in decimal, on standard output. *)
30

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
31 32
  (*i val print_real (r:real) : unit *)
  (*i prints a real number on standard output. *)
33

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
34 35 36
  (*i val print_endline (s:string) : unit *)
  (*i prints a string, followed by a newline character, on standard output
      and flushes standard output. *)
37

38 39 40 41 42 43 44
  (** 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) }
45 46 47 48

end