null.mlw 772 Bytes
Newer Older
1 2 3 4 5

(** {1 A possibly null, yet safe, value}

    The OCaml driver does optimize this into the identity.

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
6
    To permit the implementation of eq_null, null is implemented as a
7 8 9 10 11 12 13 14 15
    heap-allocated value in OCaml, e.g., Obj.magic [|0|]
*)

module Null

  type null = int

  type t_model 'a = Null null | Value 'a

16
  type t 'a = abstract { v: t_model 'a }
17

18
  let ghost predicate is_null (t: t 'a) =
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
    match t.v with Null _ -> true | Value _ -> false end

  val create_null () : t 'a
    ensures { is_null result }

  val eq_null (n x: t 'a) : bool
    requires { is_null n }
    ensures  { result <-> x.v = n.v }

  val create (x: 'a) : t 'a
    ensures { result.v = Value x }

  val get (t: t 'a) : 'a
    requires { not (is_null t) }
    ensures  { t.v = Value result }

35
end