hath995

module LL {
    ghost predicate distinct<T(==)>(items: seq<T>) {
        forall i,j :: 0<= i < j < |items| && i!=j ==> items[i] != items[j]
    }
    class Node {
        var data: int
        var next: Node?
        
        ghost var footprint: set<object>
        ghost var ancestorRepr: set<Node>

hath995

abstract module Group {
  type T(==)
  const elems : set<T>
  function identity(): (r: T)
    ensures r in elems
    ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a
  function compose(a: T, b: T): (r: T)
    requires a in elems && b in elems
    ensures r in elems
  function inverse(a: T) : (r: T)

hath995

OS X Screencast to animated GIF

This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.

Instructions

To capture the video (filesize: 19MB), using the free "QuickTime Player" application: