Linked list

Verifying several operations (e.g. append, clone, concatenate, prepend, etc.) on a linked list structure.

General Information

Backend: Chalice
Language: PVL
Features: Sequences, Lists
Path to Example File: lists/linkedlist.pvl
Should Verify: Yes
Date: 2017-06-20
Lines of Code: 215 (comments not included)
Lines of Specification: 98 (45.6% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases LinkedList
//:: tools silicon
//:: verdict Pass

/** Contains helper methods for integer sequences */
class Seq {
	/** appends an integer `v` to the front of the sequence `s` */
	pure static seq<int> append(int v, seq<int> s) = seq<int> { v } + s;
	
	/** gives an empty integer sequence */
	pure static seq<int> create_empty() = seq<int> { };
	
	/** tests whether the given sequence `s` is empty */
	pure static boolean is_empty(seq<int> s) = s == Seq.create_empty();
	
	/** prepends an integer `v` to the back of the sequence `s` */
	pure static seq<int> prepend(int v, seq<int> s) = s + seq<int> { v };
	
	/** removes the first occurence of `v` in `s`. */
	pure static seq<int> `remove`(seq<int> s, int v) = Seq.is_empty(s) ? Seq.create_empty() :
		(head(s) == v ? tail(s) : Seq.append(head(s), `remove`(tail(s), v)));
		
	/** gives the reverse of `s`. */
	pure static seq<int> reverse(seq<int> s) = Seq.is_empty(s) ? Seq.create_empty() : Seq.reverse(tail(s)) + seq<int> { head(s) };
}

class List {
	List next;
	int value;
	
	resource state(frac p) = p != none ** Perm(value, p) ** Perm(next, p) ** next->state(p);
	
	/** tests whether `list` is empty. */
	pure static boolean is_empty(List list) = list == null;
	
	/** yields a sequence containing the values of `list`. */
	requires p != none ** list->state(p);
	pure static seq<int> as_seq(List list, frac p) =
		List.is_empty(list) ? Seq.create_empty() : \unfolding list.state(p) \in seq<int> { list.value } + List.as_seq(list.next, p);

/** constructs a new list with tail `n` and value `v` */
	given seq<int> orig;
	requires n->state(write);
	requires List.as_seq(n, write) == orig;
	ensures state(write);
	ensures \unfolding state(write) \in value == v;
	ensures \unfolding state(write) \in next == n;
	ensures \unfolding state(write) \in List.as_seq(next, write) == orig;
	ensures List.as_seq(this, write) == Seq.append(v, orig);
	List(List n, int v) {
		next = n;
		value = v;
		fold state(write);
	}
	
	/** gives a new list equal to `list` but with `value` appended to the front. */
	given frac p;
	given seq<int> orig;
	context p != none ** list->state(p);
	requires orig == List.as_seq(list, p);
	ensures \result != null;
	ensures \result.state(write);
	ensures value == \unfolding \result.state(write) \in \result.value;
	ensures List.as_seq(\result, write) == Seq.append(value, orig);
	static List append(List list, int value) {
		List tail_list = List.clone(list) with {
			orig = orig;
			p = p;
		};
		
		return new List(tail_list, value) with {
			orig = orig;
		};
	}
	
	/** yields a clone (hard copy) of the input list `a`. */
	given frac p;
	given seq<int> orig;
	context p != none ** a->state(p);
	requires orig == List.as_seq(a, p);
	ensures \result->state(write);
	ensures List.as_seq(\result, write) == orig;
	static List clone(List a) {
		if (List.is_empty(a)) {
			return null;
		}
		
		unfold a.state(p);
		
		List rec = clone(a.next) with {
			orig = tail(orig);
			p = p;
		};

List result = new List(rec, a.value) with {
			orig = List.as_seq(rec, write);
		};
		
		fold a.state(p);
		return result;
	}
	
	/** returns a list that represents the concatenation of `a` with `b`. */
	given frac p;
	given frac q;
	given seq<int> orig_a;
	given seq<int> orig_b;
	context p != none ** q != none ** a->state(p) ** b->state(q);
	requires orig_a == List.as_seq(a, p);
	requires orig_b == List.as_seq(b, q);
	ensures \result->state(write);
	ensures List.as_seq(\result, write) == orig_a + orig_b;
	static List concatenate(List a, List b) {
		if (List.is_empty(a)) {
			return List.clone(b) with {
				orig = orig_b;
				p = q;
			};
		}
		
		unfold a.state(p);
		
		List rec = concatenate(a.next, b) with {
			orig_a = List.as_seq(a.next, p);
			orig_b = List.as_seq(b, q);
			p = p;
			q = q;
		};
		
		List result = new List(rec, a.value) with {
			orig = List.as_seq(rec, write);
		};
		
		fold a.state(p);
		return result;
	}
	
	/** prepends `value` to the back of `list`. */
	given frac p;
	given seq<int> orig;
	context p != none ** list->state(p);
	requires List.as_seq(list, p) == orig;
	ensures \result != null;
	ensures \result.state(write);
	ensures List.as_seq(\result, write) == Seq.prepend(value, orig);
	static List prepend(List list, int value) {
		if (List.is_empty(list)) {
			return new List(null, value) with {
				orig = Seq.create_empty();
			};
		}
		
		unfold list.state(p);
		
		List rec = prepend(list.next, value) with {
			orig = tail(orig);
			p = p;
		};
		
		List result = new List(rec, list.value) with {
			orig = List.as_seq(rec, write);
		};
		
		fold list.state(p);
		return result;
	}
	
	
	/** gives a new list equal to `list` but with the first occurence of `value` removed. */
	given frac p;
	given seq<int> orig;
	context p != none ** list->state(p);
	requires orig == List.as_seq(list, p);
	ensures \result->state(write);
	ensures List.as_seq(\result, write) == Seq.`remove`(orig, value);
	static List `remove`(List list, int value) {
		if (List.is_empty(list)) {
			return null;
		}
		
		unfold list.state(p);
		
		if (list.value == value) {
			List result = List.clone(list.next) with {
				orig = tail(orig);
				p = p;
			};
			
			fold list.state(p);
			return result;
		}
		
		List rec = `remove`(list.next, value) with {
			orig = tail(orig);
			p = p;
		};
		
		List result = new List(rec, list.value) with {
			orig = List.as_seq(rec, write);
		};
		
		fold list.state(p);
		return result;
	}

/** gives a new list equal to the reversed `list`. */
	given frac p;
	given seq<int> orig;
	context p != none ** list->state(p);
	requires orig == List.as_seq(list, p);
	ensures \result->state(write);
	ensures List.as_seq(\result, write) == Seq.reverse(orig);
	static List reverse(List list) {
		if (List.is_empty(list)) {
			return null;
		}
		
		unfold list.state(p);
		
		List rec = List.reverse(list.next) with {
			orig = tail(orig);
			p = p;
		};
		
		// this should be done nice when we have the non-static members!
		List result = List.prepend(rec, list.value) with {
			orig = List.as_seq(rec, write);
			p = write;
		};
		
		fold list.state(p);
		return result;
	}
}

Language: