Library frag_list_reverse_list

Require Import Omega List ZArith EqNat.
Require Import bipl.
Require Import seplog.
Require Import frag_list_entail.
Require Import frag_list_triple.
Require Import frag_list_vcg.
Require Import expr_b_dp.

Require Import integral_type.

Import seplog_Z_m.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.assert_m.

Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_hoare_scope.
Local Open Scope frag_list_vc_scope.

Import ZIT.

Coercion var_e : var.v >-> expr.
Coercion nat_e : nat >-> expr.

Local Close Scope Z_scope.

Definition next := 0%Z.
Definition data := 1%Z.
Definition i : var.v := 2.
Definition j : var.v := 3.
Definition k : var.v := 4.

Definition reverse_list_precond := (true_b, lst i 0) :: nil.

Definition reverse_list_postcond := (true_b, lst j 0) :: nil.

Definition invariant :=
  (i =e 0 , lst j 0) ::
  (i <>e 0, star (lst i 0) (lst j 0)) ::
  nil.

Definition invariant_auto :=
  ((i <>e 0) &e (j =e 0), lst i 0) ::
  ((j <>e 0) &e (i =e k), star (lst k 0) (lst j 0)) ::
  nil.

Definition invariant2 := (true_b, star (lst i 0) (lst j 0)) :: nil.

Definition reverse_list : cmd'' :=
  (j <- 0);
  while'' (i <>e 0) invariant2 (
    (k <-* (i -.> next));
    ((i -.> next) *<- j);
    (j <- i);
    (i <- k)
  ).

Lemma reverse_list_verif_frag :
  {{ Assrt_interp reverse_list_precond }} frag_list_vcg.proj_cmd reverse_list {{ Assrt_interp reverse_list_postcond }}.
Proof.
apply frag2_hoare_correct.
compute.
reflexivity.
Qed.