This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.
To capture the video (filesize: 19MB), using the free "QuickTime Player" application:
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) |
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> |