Encoding ADTs
An encoding of a Haskell-style Nil-Cons-list, alongside proofs of certain properties of the encoded abstract data type, and a pattern match exhaustiveness check. Note that the example is supposed to yield 1 verification error (the encoding of a failed exhaustiveness check).
/* This example demonstrates how algebraic data types, in this case a
* Haskell-style Nil-Cons list
*
* data List = Nil | Cons Int List
*
* could be encoded in Silver, and how
* properties of functions over such a data type can proved.
*/
domain list {
/* Constructors */
function Nil(): list
function Cons(head: Int, tail: list): list
/* Deconstructors */
function head_Cons(xs: list): Int // requires is_Cons(xs)
function tail_Cons(xs: list): list // requires is_Cons(xs)
/* Constructor types */
function type(xs: list): Int
unique function type_Nil(): Int
unique function type_Cons(): Int
function is_Nil(xs: list): Bool
function is_Cons(xs: list): Bool
/* Axioms */
axiom destruct_over_construct_Cons {
forall head: Int, tail: list :: {Cons(head, tail)}
head_Cons(Cons(head, tail)) == head
&& tail_Cons(Cons(head, tail)) == tail
}
axiom construct_over_destruct_Cons {
forall xs: list :: {head_Cons(xs)} {tail_Cons(xs)}
is_Cons(xs) ==> xs == Cons(head_Cons(xs), tail_Cons(xs))
}
axiom type_of_Nil {
type(Nil()) == type_Nil()
}
axiom type_of_Cons {
forall head: Int, tail: list :: type(Cons(head, tail)) == type_Cons()
}
axiom type_existence {
forall xs: list ::
type(xs) == type_Nil()
|| type(xs) == type_Cons()
}
axiom type_is_Nil {
forall xs: list :: type(xs) == type_Nil() <==> is_Nil(xs)
}
axiom type_IsElem {
forall xs: list :: type(xs) == type_Cons() <==> is_Cons(xs)
}
}
/* Datatype constructors are mutually exclusive */
method test_types(x: list) {
assert is_Nil(x) <==> !is_Cons(x)
}
/* Prove some properties of lists */
method test_quantifiers() {
/* The elements of a deconstructed Cons are equivalent to the corresponding arguments of Cons */
assert forall head: Int, tail: list, xs: list ::
is_Cons(xs) ==> (head == head_Cons(xs) && tail == tail_Cons(xs) <==> Cons(head, tail) == xs)
/* Two Cons are equal iff their constructors' arguments are equal */
assert forall head1: Int, head2: Int, tail1: list, tail2: list ::
Cons(head1, tail1) == Cons(head2, tail2) <==> head1 == head2 && tail1 == tail2
}
method pattern_match_exhaustiveness_test(xs: list) {
/* Consider the following Haskel function over Nil-Cons lists:
*
* foo :: List -> Bool
*
* foo Nil = True
* foo (Cons _ Nil) = False
* foo (Cons _ (Cons _ _)) = True
*
* The following assertion, consisting of negations of the matching patterns
* that define the 'foo' function (on the left of the implication) holds
* because the 'foo' function is total, i.e. it matching patterns
* exhaustively cover all possible inputs.
*/
assert !(is_Nil(xs))
&& !(is_Cons(xs) && let ys == (tail_Cons(xs)) in is_Nil(ys))
&& !(is_Cons(xs) && let y == (head_Cons(xs)) in let ys == (tail_Cons(xs)) in is_Cons(ys))
==>
false
/* However, if we changed the last pattern to
*
* foo (Cons y (Cons z _)) | y < z = True
*
* then the corresponding pattern match exhaustiveness check *fails as expected*:
*/
assert !(is_Nil(xs))
&& !(is_Cons(xs) && let ys == (tail_Cons(xs)) in is_Nil(ys))
&& !( is_Cons(xs) && let y == (head_Cons(xs)) in let ys == (tail_Cons(xs)) in is_Cons(ys)
&& let z == (head_Cons(ys)) in y < z)
==>
false
}