(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Stack example, aliasing} *)


module Stack

  use export list.List
  use export list.HdTlNoOpt

  type stack = list int

  val push (ref s: stack) (x:int): unit
    writes { s }
    ensures { s = Cons x (old s) }

  val pop (ref s: stack) : int
    requires { s <> Nil }
    writes { s }
    ensures { s = tl (old s) /\ result = hd (old s) }

end


module Test

  use Stack

  val ref x : stack

  (** [copy_top y] pushes onto [y] the top element of [x] *)
  val copy_top (ref y: stack): unit
    requires { x <> Nil }
    reads { x }
    writes { y }
    ensures { y = Cons (hd x) (old y) }


  let test1 () : unit =
    push x 42; push x 17;
    let ref z = Nil in
    copy_top z;
    assert { hd x = 17 /\ hd (tl x) = 42 };
    assert { z = Cons 17 Nil }

(*
  let test2 () : unit =
    push x 42; push x 17;
    copy_top x;
    assert { hd (tl x) = 17 }; (* ? *)
    assert { hd (tl x) = 42 }; (* ? *)
*)

end



(*
Local Variables:
compile-command: "why3 ide stack2.mlw"
End:
*)