/************************************************************************/ /************************* BEGIN IMPLEMENTATION *************************/
/* Aux structure of linked lists */ typedef struct list_node list; struct list_node { string data; list* next; };
bool is_acyclic(list* start) { if (start == NULL) return true; list* h = start->next; // hare list* t = start; // tortoise while (h != t) { if (h == NULL || h->next == NULL) return true; h = h->next->next; //@assert t != NULL; // hare is faster and hits NULL quicker t = t->next; } //@assert h == t; return false; }
/* is_segment(start, end) will diverge if list is circular! */ bool is_segment(list* start, list* end) { if (start == NULL) return false; if (start == end) return true; return is_segment(start->next, end); }
// Will run for ever if the segment is circular void print_segment(list* start, list* end) //requires start != NULL; { for (list* p = start; p != end; p = p->next) { printf("%s", p->data); if (p != end) printf("->"); } }
/************************************************************************/ /************************* BEGIN IMPLEMENTATION *************************/
/* Aux structure of linked lists */ typedef struct list_node list; struct list_node { string data; list* next; };
bool is_acyclic(list* start) { if (start == NULL) return true; list* h = start->next; // hare list* t = start; // tortoise while (h != t) { if (h == NULL || h->next == NULL) return true; h = h->next->next; //@assert t != NULL; // hare is faster and hits NULL quicker t = t->next; } //@assert h == t; return false; }
/* is_segment(start, end) will diverge if list is circular! */ // Recursive version bool is_segment(list* start, list* end) { if (start == NULL) return false; if (start == end) return true; return is_segment(start->next, end); } // Iterative version using a while loop bool is_segmentB(list* start, list* end) { list* l = start; while (l != NULL) { if (l == end) return true; l = l->next; } return false; } // Iterative version using a for loop bool is_segmentC(list* start, list* end) { for (list* p = start; p != NULL; p = p->next) { if (p == end) return true; } return false; }
// Will run for ever if the segment is circular void print_segment(list* start, list* end) //requires start != NULL; { for (list* p = start; p != end; p = p->next) { printf("%s", p->data); if (p != end) printf("->"); } }
// Internal debugging function that prints an UBA without checking contracts // (useful to debug representation invariant issues) void uba_print_unsafe(uba* A) { printf("UBA limit=%d; length=%d; data=[", A->limit, A->size); for (int i = 0; i < A->limit; i++) //@loop_invariant 0 <= i && i <= A->limit; { if (i < A->size) printf("%s", A->data[i]); else printf("X"); if (i < A->limit-1) { if (i == A->size-1) printf(" | "); else printf(", "); } } printf("]"); }
bool is_array_expected_length(string[] A, int length) { //@assert \length(A) == length; return true; }
bool is_uba(uba* A) { return A != NULL && 0 <= A->size && A->size < A->limit && is_array_expected_length(A->data, A->limit); }
// Internal debugging function that prints an SSA // (useful to spot bugs that do not invalidate the representation invariant) void uba_print_internal(uba* A) //@requires is_uba(A); { uba_print_unsafe(A); }
// Implementation of exported functions int uba_len(uba* A) //@requires is_uba(A); //@ensures 0 <= \result && \result < \length(A->data); { return A->size; }
string uba_get(uba* A, int i) //@requires is_uba(A); //@requires 0 <= i && i < uba_len(A); { return A->data[i]; }
void uba_set(uba* A, int i, string x) //@requires is_uba(A); //@requires 0 <= i && i < uba_len(A); //@ensures is_uba(A); { A->data[i] = x; }
void uba_resize(uba* A, int new_limit) /* A may not be a valid array since A->size == A->limit is possible! */ //@requires A != NULL; //@requires 0 <= A->size && A->size < new_limit; //@requires \length(A->data) == A->limit; //@ensures is_uba(A); { string[] B = alloc_array(string, new_limit);
for (int i = 0; i < A->size; i++) //@loop_invariant 0 <= i; { B[i] = A->data[i]; }
我们有两种进行Amortized Analysis的方法。
一个比较方便的表示方法是使用token来表示操作的耗费(e.g. 1 token for push, 1 token for pop),在实际数据结构分析时判断每个操作本身所需的token和其隐含的token,这样就可以给每个操作得到固定的token值,再做平均。在对于多个操作组成的序列(e.g. push and pop from a stack)做分析时比较有用。
Identify cost of future operations to save tokens for (e.g. resizing an array, moving elements over)
How many current operations do we perform before the future operation?(divide # of tokens to save by # of current ops that lead up to the future op)
Compute amortized cost(cost of operation itself + cost saved for future ops)
entry hdict_lookup(hdict* H, key k) //@requires is_hdict(H); //@ensures \result == NULL || key_equiv(entry_key(\result), k); { int i = index_of_key(H, k); for (chain* p = H->table[i]; p != NULL; p = p->next) { if (key_equiv(entry_key(p->data), k)) return p->data; } return NULL; }
void hdict_insert(hdict* H, entry x) //@requires is_hdict(H); //@requires x != NULL; //@ensures is_hdict(H); //@ensures hdict_lookup(H, entry_key(x)) == x; { key k = entry_key(x); int i = index_of_key(H, k); for (chain* p = H->table[i]; p != NULL; p = p->next) { //@assert p->data != NULL; // From preconditions -- operational reasoning! if (key_equiv(entry_key(p->data), k)) { p->data = x; return; } }
// prepend new entry chain* p = alloc(chain); p->data = x; p->next = H->table[i]; H->table[i] = p; (H->size)++; }
// Statistics int chain_length(chain* p) { int i = 0; while (p != NULL) { i++; p = p->next; } return i; }
// report the distribution stats for the hashtable void hdict_stats(hdict* H) //@requires is_hdict(H); { int max = 0; int[] A = alloc_array(int, 11); for(int i = 0; i < H->capacity; i++) { int j = chain_length(H->table[i]); if (j > 9) A[10]++; else A[j]++; if (j > max) max = j; }
printf("Hash table distribution: how many chains have size...\n"); for(int i = 0; i < 10; i++) { printf("...%d: %d\n", i, A[i]); } printf("...10+: %d\n", A[10]); printf("Longest chain: %d\n", max); }
// Client-side type typedef hdict* hdict_t;
/************************** END IMPLEMENTATION **************************/ /************************************************************************/
C0 语言的内存模型包括局部内存、分配内存、堆(heap)、栈(stack)、文本段(TEXT),数据段(DATA)和OS。 Heap等价于alloc memory(stores local variables and function call information),Stack等价于local memory(stores data with a lifetime not tied to the function call stack, allocated and freed by the programmer),Text(contains executable code of the program), Data(stores global and static variables that are initialized with a value or values that are not explicitly initialized), 和OS(system calls, interrupts and other OS-related function)。C1 语言扩展了 C0,允许使用函数指针,即可以存储和操作指向函数的指针。使用 & 操作符获取函数的地址。将函数指针存储在变量或数据结构中。通过解引用函数指针来调用指向的函数。
函数类型的声明使用 typedef 为函数指针创建类型,如 typedef int string_to_int_fn(string s);。
/* Minimal tree representation check */ bool is_tree(tree* T) { // minimal // Code for empty tree if (T == NULL) return true;
// Code for non-empty tree return T->data != NULL && is_tree(T->left) && is_tree(T->right); }
/* is_ordered(T, lo, hi) checks if all entries in T * are strictly in the interval (lo,hi). * lo = NULL represents -infinity; hi = NULL represents +infinity */ bool is_ordered(tree* T, entry lo, entry hi) //@requires is_tree(T); { // Code for empty tree if (T == NULL) return true;
// Code for non-empty tree //@assert T->data != NULL; // because is_tree(T) key k = entry_key(T->data); return (lo == NULL || key_compare(entry_key(lo), k) < 0) && (hi == NULL || key_compare(k, entry_key(hi)) < 0) && is_ordered(T->left, lo, T->data) && is_ordered(T->right, T->data, hi); }
entry bst_lookup(tree* T, key k) //@requires is_bst(T); //@ensures \result == NULL || key_compare(entry_key(\result), k) == 0; { // Code for empty tree if (T == NULL) return NULL;
// Code for non-empty tree int cmp = key_compare(k, entry_key(T->data)); if (cmp == 0) return T->data; if (cmp < 0) return bst_lookup(T->left, k); //@assert cmp > 0; return bst_lookup(T->right, k); }
// Builds a singleton tree with just entry e tree* leaf(entry e) //@requires e != NULL; //@ensures is_bst(\result); { tree* T = alloc(tree); T->data = e; T->left = NULL; // Not necessary T->right = NULL; // Not necessary return T; }
tree* bst_insert(tree* T, entry e) //@requires is_bst(T) && e != NULL; //@ensures is_bst(\result) && \result != NULL; //@ensures bst_lookup(\result, entry_key(e)) == e; { // Code for empty tree if (T == NULL) return leaf(e);
// Code for non-empty tree int cmp = key_compare(entry_key(e), entry_key(T->data)); if (cmp == 0) T->data = e; else if (cmp < 0) T->left = bst_insert(T->left, e); else { //@assert cmp > 0; T->right = bst_insert(T->right, e); }
/* Minimal tree representation check */ bool is_tree(tree* T) { // minimal // Code for empty tree if (T == NULL) return true;
// Code for non-empty tree return T->data != NULL && is_tree(T->left) && is_tree(T->right); }
/* is_ordered(T, lo, hi) checks if all entries in T * are strictly in the interval (lo,hi). * lo = NULL represents -infinity; hi = NULL represents +infinity */ bool is_ordered(tree* T, entry lo, entry hi) //@requires is_tree(T); { // Code for empty tree if (T == NULL) return true;
// Code for non-empty tree //@assert T->data != NULL; // because is_tree(T) key k = entry_key(T->data); return (lo == NULL || key_compare(entry_key(lo), k) < 0) && (hi == NULL || key_compare(k, entry_key(hi)) < 0) && is_ordered(T->left, lo, T->data) && is_ordered(T->right, T->data, hi); }
/* UNUSED: cost is O(n) int height(tree* T) //@requires is_tree(T); //@ensures \result >= 0; { if (T == NULL) return 0; return 1 + max(height(T->left), height(T->right)); } */
tree* rebalance_right(tree* T) // T must be immediate result of a right-insertion //@requires T != NULL && T->right != NULL; //@requires is_avl(T->left) && is_avl(T->right); //@ensures is_avl(\result); { if (height(T->right) - height(T->left) == 2) { // violation! if (height(T->right->right) > height(T->right->left)) { // Single rotation T = rotate_left(T); } else { //@assert height(T->right->left) > height(T->right->right); // Double rotation T->right = rotate_right(T->right); T = rotate_left(T); } } else { // No rotation needed, but tree may have grown fix_height(T); }
return T; }
tree* rebalance_left(tree* T) // T must be immediate result of a left-insertion //@requires T != NULL && T->left != NULL; //@requires is_avl(T->left) && is_avl(T->right); //@ensures is_avl(\result); { if (height(T->left) - height(T->right) == 2) { // violation! if (height(T->left->left) > height(T->left->right)) { // Single rotation T = rotate_right(T); } else { //@assert height(T->left->right) > height(T->left->left); // Double rotation T->left = rotate_left(T->left); T = rotate_right(T); } } else { // No rotation needed, but tree may have grown fix_height(T); }
return T; }
// Builds a singleton tree with just entry e tree* leaf(entry e) //@requires e != NULL; //@ensures is_avl(\result); { tree* T = alloc(tree); T->data = e; T->left = NULL; // Not necessary T->right = NULL; // Not necessary T->height = 1; return T; }
tree* avl_insert(tree* T, entry e) //@requires is_avl(T) && e != NULL; //@ensures is_avl(\result) && \result != NULL; //@ensures avl_lookup(\result, entry_key(e)) == e; { // Code for empty tree if (T == NULL) return leaf(e);
// Code for non-empty tree //@assert is_avl(T->left); //@assert is_avl(T->right); int cmp = key_compare(entry_key(e), entry_key(T->data)); if (cmp == 0) T->data = e; else if (cmp < 0) { // Go left T->left = avl_insert(T->left, e); //@assert is_avl(T->left) && T->left != NULL && is_avl(T->right); T = rebalance_left(T); //@assert is_avl(T); } else { // Go right //@assert cmp > 0; T->right = avl_insert(T->right, e); //@assert is_avl(T->left) && is_avl(T->right) && T->right != NULL; T = rebalance_right(T); //@assert is_avl(T); }