Logical declarations

Coma admits WhyML logical declarations such as

• Module imports

  use int.Int
  use list.List as L
  

• Types

  • abstract types

    type char
    

  • aliases

    type word = seq char
    

  • algebraic data types

    type regexp =
    | Empty
    | Epsilon
    | Char    char
    | Alt     regexp regexp
    | Concat  regexp regexp
    | Star    regexp
    

• Pure functions and predicates

  function sum (f: int -> int) (a b: int): int
    variant { b - a }
  = if b <= a then 0 else sum f a (b - 1) + f (b - 1)
  

• Inductive predicates

  inductive mem (w: word) (r: regexp) =
    | mem_eps:  mem empty Epsilon
    | mem_char: forall c: char. mem (singleton c) (Char c)
    | …
  

• Lemmas and axioms

  lemma sum_left:
    forall f: int -> int, a b: int.
    a < b -> sum f a b = f a + sum f (a + 1) b
  

• …