Full linked list example

package list

type List struct {
	// Pointer to the next element in the linked list.
	next *List
	// The value stored with this element.
	Value int
}


/*@
// Represents access to the List element and all elements in its tail.
pred (l *List) Mem() {
	l != nil ==> (acc(l) && l.next.Mem())
}
@*/

// Returns the empty list.
// @ ensures l.Mem()
// @ ensures l.IsEmpty()
func Empty() (l *List) {
	l = (*List)(nil)
	// @ fold l.Mem()
	return
}

// New creates a new List node with the specified value and tail.
// @ requires tail.Mem()
// @ ensures out.Mem()
// @ ensures out.View() == seq[int]{value} ++ old(tail.View())
func New(value int, tail *List) (out *List) {
	out = &List{next: tail, Value: value}
	// @ fold out.Mem()
	return
}


// Tail returns a new list that is the tail of the original list,
// excluding the first element.
// @ requires l.Mem()
// @ requires !l.IsEmpty()
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[1:])
func (l *List) Tail() (out *List) {
	// @ unfold l.Mem()
	out = l.next
	return
}

// Remove returns the list with the element at index i deleted.
// @ requires l.Mem()
// @ requires 0 <= i && i < len(l.View())
// @ ensures out.Mem()
// @ ensures out.View() == old(l.View()[:i] ++ l.View()[i+1:])
func (l *List) Remove(i int) (out *List) {
	// @ unfold l.Mem()
	if i == 0 {
		return l.next
	}
	l.next = l.next.Remove(i - 1)
	// @ fold l.Mem()
	return l
}


// Head returns the value of the first element in the list.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ requires !l.IsEmpty()
// @ ensures value == l.View()[0]
// @ decreases
func (l *List) Head() (value int) {
	return /*@ unfolding acc(l.Mem(), 1/2) in @*/ l.Value
}


// Get returns the element at index i in the list.
// @ preserves acc(l.Mem(), 1/2)
// @ preserves 0 <= i && i < len(l.View())
// @ ensures value == l.View()[i]
// @ decreases l.Mem()
func (l *List) Get(i int) (value int) {
	// @ unfold acc(l.Mem(), 1/2)
	if i == 0 {
		value = l.Value
	} else {
		value = l.next.Get(i - 1)
	}
	// @ fold acc(l.Mem(), 1/2)
	return
}


// Returns true iff the list is empty.
// @ pure
// @ requires acc(l.Mem(), 1/2)
// @ ensures empty == (len(l.View()) == 0)
// @ decreases
func (l *List) IsEmpty() (empty bool) {
	return l == nil
}


// Returns the length of the list.
// @ preserves acc(l.Mem(), 1/2)
// @ ensures length == len(l.View())
// @ decreases l.Mem()
func (l *List) Length() (length int) {
	if l == nil {
		return 0
	} else {
		// @ unfold acc(l.Mem(), 1/2)
		length = 1 + l.next.Length()
		// @ fold acc(l.Mem(), 1/2)
		return length
	}
}


/*@
ghost
pure
requires acc(l.Mem(), 1/2)
decreases l.Mem()
func (l *List) View() seq[int] {
	return l == nil ? seq[int]{} : unfolding acc(l.Mem(), 1/2) in seq[int]{l.Value} ++ l.next.View()
}
@*/

func client() {
	ll := Empty()
	l0 := ll.Length()
	// @ assert l0 == 0
	ll = New(11, ll)
	// @ assert ll.Mem()
	// @ assert ll.Head() == 11
	// @ assert ll.View() == seq[int]{11}
	l1 := ll.Length()
	// @ assert l1 == 1
	ll = ll.Tail()
	// @ assert ll.View() == seq[int]{}
	ll = New(22, Empty())
	// @ assert ll.Head() == 22
	ll = New(33, ll)
	// @ assert ll.Head() == 33
	l2 := ll.Length()
	// @ assert l2 == 2
	v0 := ll.Get(0)
	v1 := ll.Get(1)
	// @ assert v0 == 33
	// @ assert v1 == 22
	ll := ll.Remove(1)
	l3 := ll.Length()
	// @ assert ll.Head() == 33
	// @ assert l3 == 1
}