adt.vpr

// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/


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

  function size(xs:list): Int

  /* Axioms */

  axiom eitherConsorNil{
    forall xs: list ::
    is_Nil(xs) <==> !is_Cons(xs)
  }


  axiom numberOfElem{
    forall xs: list ::
        is_Nil(xs) == (size(xs) == 0)
     && is_Cons(xs) == (size(xs) > 0)
     && is_Cons(xs) == size(xs) > size(tail_Cons(xs))
     && is_Cons(xs) ==   (size(xs) == 1 + size(tail_Cons(xs)))
  }

  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)
  }
}


function f(xs:list) : Int
decreases size(xs)
requires size(xs)>=0
{
    size(xs) > 0 ? f(tail_Cons(xs)) : 6
}