1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

#include <vcc.h>
#include <stdlib.h>

typedef 
/*D_tag node */
struct node {
  int key;
  struct node * next;
} SNnode;

/*D_defs
define pred sll^(x): 
  ( 
  ((x l= nil) & emp) | 
  ((x |-> loc next: nxt) * sll^(nxt))  
  ) ;
  
define set-fun keys^(x):
  (case (x l= nil): emptyset;
   case ((x |-> loc next: nxt; int key: ky) * true): 
    ((singleton ky) union keys^(nxt));
   default: emptyset
  ) ;
*/

_(dryad)
SNnode * sll_reverse(SNnode * x)
  /*D_requires sll^(x) */
  /*D_ensures (sll^(ret) & (keys^(ret) s= old(keys^(x)))) */
{
  SNnode * acc = NULL;
  while (x != NULL)
  /*D_invariant ((sll^(x) * sll^(acc)) & ((keys^(x) union keys^(acc)) s= old(keys^(x)))) */
  {
    SNnode * tmp = x->next;
    x->next = acc;
    acc = x;
    x = tmp;
  }
  return acc;
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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

** ** In-Place Singly-Linked List Reverse *)

Fixpoint sll (ls : list W) (p : W) : HProp :=
  match ls with
    | nil => [| p = 0 |]
    | x :: ls' => [| p <> 0 |] * Ex p', (p ==*> x, p') * sll ls' p'
  end%Sep.

Theorem sll_extensional : forall ls (p : W), HProp_extensional (sll ls p).
Proof.
  destruct ls; reflexivity.
Qed.
Hint Immediate sll_extensional.

Theorem nil_fwd : forall ls (p : W), p = 0
  -> sll ls p ===> [| ls = nil |].
Proof.
  destruct ls; sepLemma.
Qed.

Theorem nil_bwd : forall ls (p : W), p = 0
  -> [| ls = nil |] ===> sll ls p.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_fwd : forall ls (p : W), p <> 0
  -> sll ls p ===> Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_bwd : forall ls (p : W), p <> 0
  -> (Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p') ===> sll ls p.
Proof.
  destruct ls; sepLemma;
    match goal with
      | [ H : _ :: _ = _ :: _ |- _ ] => injection H; sepLemma
    end.
Qed.

Definition hints : TacPackage.
  prepare (nil_fwd, cons_fwd) (nil_bwd, cons_bwd).
Defined.


Definition revS := SPEC("x") reserving 3
  Al ls,
  PRE[V] sll ls (V "x")
  POST[R] sll (rev ls) R.

Definition revM := bmodule "rev" {{
  bfunction "rev"("x", "acc", "tmp1", "tmp2") [revS]
    "acc" <- 0;;
    [Al ls, Al accLs,
      PRE[V] sll ls (V "x") * sll accLs (V "acc")
      POST[R] sll (rev_append ls accLs) R ]
    While ("x" <> 0) {
      "tmp2" <- "x";;
      "tmp1" <- "x" + 4;;
      "x" <-* "tmp1";;
      "tmp1" *<- "acc";;
      "acc" <- "tmp2"
    };;
    Return "acc"
  end
}}.

Hint Rewrite <- rev_alt : sepFormula.

Theorem revMOk : moduleOk revM.
Proof.
  vcgen; sep hints.
Qed.