list_rev.mlw 11 KB
Newer Older
1 2 3 4

module M

  use import int.Int
5
  use import module ref.Ref
6
  use import map.Map
7

8
  (** Memory model and definition of is_list *)
9
  type pointer
10
  type next = map pointer pointer
11 12
  logic null : pointer

13
  parameter value : ref (map pointer int)
14
  parameter next : ref (next)
15

16
  inductive is_list (next : next) (p : pointer) =
17 18
    | is_list_null:
        forall next : next, p : pointer.
19
        p = null -> is_list next p
20 21
    | is_list_next:
        forall next : next, p : pointer.
22 23
        p <> null -> is_list next (get next p) -> is_list next p

24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  (** Frame for is_list *)
  type ft 'a
  logic in_ft pointer (ft pointer)
  logic list_ft (next : next) (p : pointer) : ft pointer

  axiom frame_list :
    forall next : next, p : pointer, q : pointer, v : pointer
      [is_list (set next q v) p].
    (~ in_ft q (list_ft next p)) -> is_list next p
      -> is_list (set next q v) p

  (** Definition of sep_node_list *)
  logic sep_node_list (next : next) (p1 p2 : pointer) =
    ~in_ft p1 (list_ft next p2)

  axiom list_ft_node_null :
      forall next : next, q : pointer, p : pointer.
      q=null -> ~ in_ft p (list_ft next q)

  axiom list_ft_node_next1 :
      forall next : next, q : pointer, p : pointer.
      q<>null -> is_list next (get next q) ->
      in_ft p (list_ft next (get next q)) ->
      in_ft p (list_ft next q)

  axiom list_ft_node_next2 :
      forall next : next, q : pointer.
      q<>null -> is_list next (get next q) ->
      in_ft q (list_ft next q)

  axiom list_ft_node_next_inv :
      forall next : next, q : pointer, p : pointer.
      q<>null -> is_list next (get next q) ->
      q <> p ->
      in_ft p (list_ft next q) ->
      in_ft p (list_ft next (get next q))

  (** Frame for list_ft *)
  axiom frame_list_ft :
    forall next : next, p : pointer, q : pointer, v : pointer.
    (~ in_ft q (list_ft next p)) ->
      list_ft next p = list_ft (set next q v) p

  (** Definition of sep_list_list *)

  inductive list_disj (ft : ft pointer) (next : next)
  (p : pointer) =
    | list_disj_null:
        forall ft : ft pointer, next : next, p : pointer.
        p=null -> list_disj ft next p
    | list_disj_next:
        forall ft : ft pointer, next : next, p : pointer.
        p<>null -> is_list next (get next p) -> (~in_ft p ft) ->
        list_disj ft next (get next p) -> list_disj ft next p

  logic sep_list_list (next : next) (p1 p2 : pointer) =
    list_disj (list_ft next p1) next p2 /\ list_disj (list_ft next p2) next p1

  axiom list_ft_disj_null :
      forall next : next, q : pointer, p : pointer.
      q=null -> list_disj (list_ft next q) next p

  axiom list_ft_disj_next :
      forall next : next, p : pointer, q : pointer.
        q <> null -> is_list next (get next q) ->
        (~in_ft q (list_ft next p)) ->
        q <> p ->
        list_disj (list_ft next (get next q)) next p ->
        list_disj (list_ft next q) next p
93

94 95 96 97 98
  axiom list_ft_disj_next_inv :
      forall next : next, p : pointer, q : pointer.
        q <> null -> is_list next (get next q) ->
        list_disj (list_ft next q) next p ->
        list_disj (list_ft next (get next q)) next p
99

100 101 102 103 104 105 106 107 108 109 110 111 112 113
  (** Frame for list_disj *)
  axiom frame_list_disj :
    forall ft : ft pointer, next : next,
        p1 : pointer, p2 : pointer, q : pointer, v : pointer
        [list_disj (list_ft (set next q v) p1) (set next q v) p2].
      (~ in_ft q (list_ft next p1)) -> (~ in_ft q (list_ft next p2))
      -> list_disj (list_ft next p1) next p2
      -> list_disj (list_ft (set next q v) p1) (set next q v) p2

  lemma acyclic_list : forall next : next, p : pointer.
    p <> null -> is_list next p -> sep_node_list next p (get next p)

  goal consistent : forall next : next, p: pointer, q: pointer.
    is_list next p -> is_list next q -> false
114 115

  let list_rev (p : ref pointer) =
116
    { is_list !next !p }
117 118
    let q = ref null in
    while !p <> null do
119 120
      invariant
        { is_list !next !p /\ is_list !next !q /\ sep_list_list !next !p !q }
121 122 123 124 125 126
      let tmp = get !next !p in
      next := set !next !p !q;
      q := !p;
      p:= tmp
    done;
    q
127
    { is_list !next !result }
128

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
  (** behavior *)

  use import list.Append
  use import list.Reverse

  logic model (next : next) (p : pointer) : list pointer
  (* axiom model_def : forall next : next, p : pointer. *)
  (*   model next p = *)
  (*       if p = null then Nil else Cons p (model next (get next p)) *)

  axiom model_def1 : forall next : next, p : pointer[model next p].
    p = null -> model next p = Nil

  axiom model_def2 : forall next : next, p : pointer[model next p].
    p <> null -> model next p = Cons p (model next (get next p))

  lemma reverse_append : forall l1 : list 'a, l2 : list 'a, x : 'a
    [(reverse (Cons x l1)) ++ l2|(reverse l1) ++ (Cons x l2)].
  (reverse (Cons x l1)) ++ l2 = (reverse l1) ++ (Cons x l2)

  (** frame model *)
  axiom frame_model :
    forall ft : ft pointer, next : next,
    p : pointer, q : pointer, v : pointer[model (set next q v) p].
    (~ in_ft q (list_ft next p))
    -> model next p = model (set next q v) p

  let list_rev_behv (p : ref pointer) =
157
    { is_list !next !p }
158 159 160 161
    let old_next = !next in
    let old_p = !p in
    let q = ref null in
    while !p <> null do
162 163
      invariant { is_list !next !p /\ is_list !next !q
                  /\ sep_list_list !next !p !q /\
164
      reverse (model (old_next) (old_p)) =
165
       (reverse (model !next !p)) ++ (model !next !q)}
166 167 168
      let tmp = get !next !p in
      let bak_next = !next in
      next := set !next !p !q;
169 170
      assert { (reverse (Cons !p (model !next tmp))) ++ (model !next !q) =
               (reverse (model !next tmp)) ++ (Cons !p (model !next !q))};
171 172 173 174
      q := !p;
      p:= tmp
    done;
    q
175 176
    { is_list !next !result /\ reverse (model (old !next) (old !p)) =
        model !next !result}
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206


end


module M2

  use import int.Int
  use import module ref.Ref
  use import map.Map

  (** Memory model and definition of is_list *)
  type pointer

  axiom pointer_dec : forall p1:pointer, p2 : pointer. p1 = p2 or p1 <> p2

  type next = map pointer pointer
  logic null : pointer

  parameter value : ref (map pointer int)
  parameter next : ref (next)

  inductive is_list (next : next) (p : pointer) =
    | is_list_null:
        forall next : next, p : pointer.
        p = null -> is_list next p
    | is_list_next:
        forall next : next, p : pointer.
        p <> null -> is_list next (get next p) -> is_list next p

207 208 209 210
  goal is_list_disjoint_case :
      forall next : next, p : pointer.
        p = null /\ p <> null /\ is_list next (get next p) -> false

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
  (** Frame for is_list *)
  type ft 'a

  logic in_ft (p:pointer) (ft:ft pointer)

  axiom set_eq : forall ft1: ft pointer, ft2: ft pointer
    [in_ft null ft1,in_ft null ft1].
    (forall q : pointer. in_ft q ft1 <-> in_ft q ft2) -> ft1 = ft2

  logic list_ft (next : next) (p : pointer) : ft pointer

  (* axiom list_ft_node_null : *)
  (*     forall next : next, q : pointer. *)
  (*     q=null -> list_ft next q = S.empty *)

  (* axiom list_ft_node_next : *)
  (*     forall next : next, q : pointer. *)
  (*     q<>null -> is_list next (get next q) -> *)
  (*     S.add q (list_ft next (get next q)) =  (list_ft next q) *)

  axiom list_ft_node_null_cor :
      forall next : next, q : pointer,p : pointer.
      q=null -> ~in_ft p (list_ft next q)

  axiom list_ft_node_next1 :
      forall next : next, q : pointer, p : pointer.
      q<>null -> is_list next (get next q) ->
      in_ft p (list_ft next (get next q)) ->
      in_ft p (list_ft next q)

  axiom list_ft_node_next2 :
      forall next : next, q : pointer.
      q<>null -> is_list next (get next q) ->
      in_ft q (list_ft next q)

  axiom list_ft_node_next_inv :
      forall next : next, q : pointer, p : pointer.
      q<>null -> is_list next (get next q) ->
      q <> p ->
      in_ft p (list_ft next q) ->
      in_ft p (list_ft next (get next q))

  lemma frame_list :
    forall next : next, p : pointer, q : pointer, v : pointer
      [is_list (set next q v) p].
    (~ in_ft q (list_ft next p)) -> is_list next p
      -> is_list (set next q v) p

  (** Definition of sep_node_list *)
  logic sep_node_list (next : next) (p1 p2 : pointer) =
    ~in_ft p1 (list_ft next p2)

  (** Frame for list_ft *)
  lemma frame_list_ft :
    forall next : next, p : pointer, q : pointer, v : pointer.
    (~ in_ft q (list_ft next p)) -> is_list next p ->
      list_ft next p = list_ft (set next q v) p

  (** Definition of sep_list_list *)

  (* logic sep_list_list (next : next) (p1 p2 : pointer) = *)
  (*     S.inter (list_ft next p1) (list_ft next p2) = S.empty *)

  logic sep_list_list (next : next) (p1 p2 : pointer) =
     forall q : pointer.
       (~ in_ft q (list_ft next p1)) \/ (~in_ft q (list_ft next p2))

  lemma acyclic_list : forall next : next, p : pointer.
    p <> null -> is_list next p -> sep_node_list next p (get next p)

  goal consistent : forall next : next, p: pointer, q: pointer.
    is_list next p -> is_list next q -> false

  let list_rev (p : ref pointer) =
285
    { is_list !next !p }
286 287
    let q = ref null in
    while !p <> null do
288 289
      invariant
        { is_list !next !p /\ is_list !next !q /\ sep_list_list !next !p !q }
290 291 292 293 294 295
      let tmp = get !next !p in
      next := set !next !p !q;
      q := !p;
      p:= tmp
    done;
    q
296
    { is_list !next !result }
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328

  (** behavior *)

  use import list.Append
  use import list.Reverse

  (* meta "encoding : lskept" logic Cons *)
  (* meta "encoding : lskept" logic Nil *)

  logic model (next : next) (p : pointer) : list pointer
  (* axiom model_def : forall next : next, p : pointer[model next p]. *)
  (*   model next p = *)
  (*       if p = null then Nil else Cons p (model next (get next p)) *)

  axiom model_def1 : forall next : next, p : pointer[model next p].
    p = null -> model next p = Nil

  axiom model_def2 : forall next : next, p : pointer[model next p].
    p <> null -> model next p = Cons p (model next (get next p))

  (** frame model *)
  lemma frame_model :
    forall ft : ft pointer, next : next,
    p : pointer, q : pointer, v : pointer[model (set next q v) p].
    is_list next p ->
    (~ in_ft q (list_ft next p)) ->
    model next p = model (set next q v) p

  goal consistent_behv : forall next : next, p: pointer, q: pointer.
    is_list next p -> is_list next q -> false

  let list_rev_behv (p : ref pointer) =
329
    { is_list !next !p }
330 331 332
    let old_next = !next in
    let old_p = !p in
    let q = ref null in
333
    label Init:
334
    while !p <> null do
335 336
      invariant { is_list !next !p /\ is_list !next !q
                  /\ sep_list_list !next !p !q /\
337
      reverse (model (at !next Init) (old_p)) =
338
       (reverse (model !next !p)) ++ (model !next !q)}
339 340 341
      let tmp = get !next !p in
      let bak_next = !next in
      next := set !next !p !q;
342 343
      (* assert { (reverse (Cons p (model !next tmp))) ++ (model !next q) = *)
      (*          (reverse (model !next tmp)) ++ (Cons p (model !next q))}; *)
344 345 346 347
      q := !p;
      p:= tmp
    done;
    q
348 349
    { is_list !next !result /\ reverse (model (old !next) (old !p)) =
        model !next !result}
350

351 352 353
end

(*
354
Local Variables:
355
compile-command: "unset LANG; make -C ../.. examples/programs/list_rev.gui"
356
End:
357
*)