Jump to content

User:Rgrig

From Wikipedia, the free encyclopedia

Experiments

[edit]
typedef struct Node {
  struct Node* next;
  void* data;
} Node;

// Pre: list(x)
// Post: list(return)
Node* list_reverse(Node* x) {
  Node* y; // result
  Node* z; // auxiliary variable
  
  // list(x)
  y = NULL;
  // list(x) /\ y = NULL
  while (x != NULL) 
    // Inv: list(y) * list(x)
  {
    // (list(y) * list(x)) /\ x != NULL
    // list(y) * x |-> x' * list(x')
    z = x->next; 
    // list(y) * x |-> z * list(z)
    x->next = y;
    // list(y) * x |-> y * list(z)
    y = x;
    // list(y') * y |-> y' * list(z)
    // list(y) * list(z)
    x = z;
    // list(y) * list(x)
  }
  // (list(y) * list(x)) /\ x = NULL
  // list(y) /\ x = NULL
  return y;
}