Rgrig

This is a Wikipedia user page.
This is not an encyclopedia article or the talk page for an encyclopedia article. If you find this page on any site other than Wikipedia, you are viewing a mirror site. Be aware that the page may be outdated and that the user whom this page is about may have no personal affiliation with any site other than Wikipedia. The original page is located at https://en.wikipedia.org/wiki/User:Rgrig.

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;
}