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

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


module Stack

  use export list.List
  use export list.HdTlNoOpt (* hd and tl operators *)

  type stack = list int

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

  let pop (ref s: stack) : int
    requires { s <> Nil }
    writes  { s }
    ensures { s = tl (old s) /\ result = hd (old s) }
  = match s with
    | Nil -> absurd
    | Cons x r -> s <- r; x
    end

end



module Test

  use Stack

  val ref s1: stack
  val ref s2: stack

  let test () : int
    writes { s1,s2 }
    ensures { result = 13 /\ hd s2 = 42 }
  = push s1 13; push s2 42; pop s1



  let test2 (ref s3 s4: stack) : unit
    writes { s3,s4 }
    ensures { hd s3 = 13 /\ hd s4 = 42 }
  = push s3 13; push s4 42

(*
  let test3 (ref s5: stack) : unit
    writes { s5 }
    ensures { hd s5 = 13 /\ hd s5 = 42 }
  = test2 s5 s5
*)

end


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