Commit 0f26787c authored by Mário Pereira's avatar Mário Pereira

New file ocaml.mlw in modules

parent ce8cd6d7
(* module OCaml *)
(* use export int.Int *)
(* use export int.MinMax *)
(* use export option.Option *)
(* use export list.List *)
(* use export seq.Seq *)
(* scope Sys *)
(* constant max_array_length : int *)
(* end *)
(* use array.Array *)
(* type array 'a = Array.array 'a *)
(* end *)
module Sys
use import int.Int
use import mach.int.Int63
val constant max_array_length : int63
axiom non_neg_max_array_length : to_int max_array_length >= 0
end
module Pervasives
exception Exit
use import int.Int
use import mach.int.Int63
val succ (x: int63) : int63
requires { "expl:integer overflow" in_bounds (to_int x + 1) }
ensures { to_int result = to_int x + 1 }
val pred (x: int63) : int63
requires { "expl:integer overflow" in_bounds (to_int x - 1) }
ensures { to_int result = to_int x - 1 }
end
\ No newline at end of file
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