(Added categories "How to" and "Tools")
|(25 intermediate revisions by one user not shown)|
Latest revision as of 15:52, 22 February 2012
 1 Introduction
Zeno is an automated proof system for Haskell program properties; developed at Imperial College London by William Sonnex, Sophia Drossopoulou and Susan Eisenbach. It aims to solve the general problem of equality between two Haskell terms, for any input value.
Many program verification tools available today are of the model checking variety; able to traverse a very large but finite search space very quickly. These are well suited to problems with a large description, but no recursive datatypes. Zeno on the other hand is designed to inductively prove properties over an infinite search space, but only those with a small and simple specification.
One can try Zeno online at TryZeno, or cabal install zeno to use it from home. You can find the latest paper on Zeno here, though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.
 1.1 Features
- Outputs proofs and translated Haskell programs to an Isabelle/HOL theory file and will automatically invoke Isabelle to check it (requires isabelle to be visible on the command line).
- Works with full Haskell98 along with any GHC extensions not related to the type system. Unfortunately not all Haskell code is then convertable to Isabelle/HOL, see Zeno#Limitations for details.
- Has a built-in counter-example finder, along the same lines as SmallCheck, but using symbolic evaluation to control search depth.
- Its property language is just a Haskell DSL.
 2 Example Usage
The first thing you need is the Zeno.hs file which contains the definitions for Zeno's property DSL. It should be in your Zeno installation directory but is also given below:
module Zeno ( Bool (..), Equals (..), Prop, prove, proveBool, given, givenBool, ($), otherwise ) where import Prelude ( Bool (..) ) infix 1 :=: infixr 0 $ ($) :: (a -> b) -> a -> b f $ x = f x otherwise :: Bool otherwise = True data Equals = forall a . (:=:) a a data Prop = Given Equals Prop | Prove Equals prove :: Equals -> Prop prove = Prove given :: Equals -> Prop -> Prop given = Given proveBool :: Bool -> Prop proveBool p = Prove (p :=: True) givenBool :: Bool -> Prop -> Prop givenBool p = Given (p :=: True)
Making sure this file is in the same directory we can now start coding:
module Test where import Prelude () import Zeno data Nat = Zero | Succ Nat length :: [a] -> Nat length  = Zero length (x:xs) = Succ (length xs) (++) :: [a] -> [a] -> [a]  ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys) class Num a where (+) :: a -> a -> a instance Num Nat where Zero + y = y Succ x + y = Succ (x + y)
Notice we have stopped any
The following code will express that the length of two appended lists is the sum of their individual lengths:
prop_length xs ys = prove (length (xs ++ ys) :=: length xs + length ys)
Add this to the above code and save it to Test.hs. We can now check
class Eq a where (==) :: a -> a -> Bool instance Eq Nat where Zero == Zero = True Succ x == Succ y = x == y _ == _ = False prop_eq_ref :: Nat -> Prop prop_eq_ref x = prove (x == x :=: True)
We have provided the helper function
prop_eq_ref x = proveBool (x == x)
We can also express implication in our properties, using the
elem :: Eq a => a -> [a] -> Bool elem _  = False elem n (x:xs) | n == x = True | otherwise = elem n xs prop_elem :: Nat -> [Nat] -> [Nat] -> Prop prop_elem n xs ys = givenBool (n `elem` ys) $ proveBool (n `elem` (xs ++ ys))
 3 Limitations
 3.1 Isabelle/HOL output
While Zeno is able to reason about any valid Haskell definition, not all of these can be converted to Isabelle for checking. There are two main restrictions:
- No internal recursive definitions; don't put recursive functions inside your functions.
- No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value. Isabelle will check for termination but Zeno will not, unfortunately this means that Zeno could be thrown into an infinite loop with such a definition.
While the above restrictions are founded in Isabelle's input language there are a few which are just laziness on part of Zeno's developers, and on our to-do list:
- No partial definitions; only use total pattern matches.
- No mututally recursive datatypes.
- No tuple types beyond quadruples.
- No name clashes, even across modules. Zeno will automatically strip module names in its output for clarity, and we have not yet implemented a flag to control this.
If you are wondering why a certain bit of code cannot be converted to Isabelle try running Zeno with the --print-core flag, this will output Zeno's internal representation for your code.
 3.2 Primitive TypesZeno can only reason about inductive datatypes, meaning the only built-in types it can use are lists, tuples and
 3.3 Infinite and undefined valuesWhen we said that Zeno proves properties of Haskell programs this wasn't entirely true, it only proves those for which every value is finite and well-defined. For example, Zeno can prove
You might ask why this is a Haskell theorem prover, rather than an ML one, if it cannot deal with infinite values, which would be a very valid question. As it stands Zeno is more a base-line for us to start more advanced research into lazy functional program verification, which will include attempting to tackle this issue.