1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(** {1 Basic I/O Functions} *)
module StdIO
use string.String
use string.Char
use int.Int
(** small trick so that printing vals are extracted to OCaml *)
type t = private {ghost mutable foo:int}
val ghost bar:t
(** prints a string to the standard output *)
val print_string (s: string) : unit
writes { bar }
(** prints a char to the standard output *)
val print_char (c: char) : unit
writes { bar }
(** prints a newline character to the standard output, and flushes it *)
val print_newline (_u:unit) : unit
writes { bar }
(** prints a Why3 int to the standard output *)
val print_int (i: int) : unit
writes { bar }
(***
use int.Int
use list.List
use list.Reverse
use ref.Ref
type prdata = PrChar char | PrInt int
(** ghost references to represent the standard output *)
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
(** 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) }
val print_string (s:string) : unit
(** prints a string on standard output. *)
val print_int (n: int) : unit
writes { cur_pos, current_line }
(** prints an integer, in decimal, on standard output. *)
val print_real (r:real) : unit
(** prints a real number on standard output. *)
val print_endline (s:string) : unit
(** prints a string, followed by a newline character, on standard output
and flushes standard output. *)
(** 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 (old !current_line)) (old !flushed) }
*)
end
|
