# Zeno

### From HaskellWiki

(Created the wiki page for Zeno.) |
m |
||

Line 14: | Line 14: | ||

* Outputs proofs and translated Haskell programs to an Isabelle/HOL theory file and will automatically invoke [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle] to check it (requires <tt>isabelle</tt> to be visible on the command line). | * Outputs proofs and translated Haskell programs to an Isabelle/HOL theory file and will automatically invoke [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle] to check it (requires <tt>isabelle</tt> 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# | + | * 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#Caveats]] for details. |

* Its property language is a Haskell DSL, so should be relatively intuitive. | * Its property language is a Haskell DSL, so should be relatively intuitive. | ||

Line 47: | Line 47: | ||

</haskell><br/> | </haskell><br/> | ||

− | Notice we have stopped any <hask>Prelude</hask> functions from being imported, this is important as we have no source code available for them; Zeno can only work with functions for which it can see the definition. The only built in | + | Notice we have stopped any <hask>Prelude</hask> functions from being imported, this is important as we have no source code available for them; Zeno can only work with functions for which it can see the definition. The only built in Haskell types we have are lists, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you. |

Now that we have some code we can define a property about this code. Properties are built through equality between terms, using the <hask>(:=:)</hask> constructor defined in <tt>Zeno.hs</tt>. We then pass this to the <hask>prove</hask> function to turn an equality into a property (<hask>Prop</hask>). We recommended looking at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short). | Now that we have some code we can define a property about this code. Properties are built through equality between terms, using the <hask>(:=:)</hask> constructor defined in <tt>Zeno.hs</tt>. We then pass this to the <hask>prove</hask> function to turn an equality into a property (<hask>Prop</hask>). We recommended looking at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short). | ||

Line 81: | Line 81: | ||

</haskell><br/> | </haskell><br/> | ||

− | We can also | + | We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions: |

<haskell> | <haskell> | ||

Line 124: | Line 124: | ||

=== Infinite and undefined values === | === Infinite and undefined values === | ||

− | + | When 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 <hask>reverse (reverse xs) = xs</hask>, which is not true for infinite lists, as <hask>xs</hask> could still be pattern matched upon, whereas evaluating <hask>reverse (reverse xs)</hask> starts an infinite loop (<hask>undefined</hask>). | |

Another example (courtesy of Tillmann Rendel) is <hask>takeWhile p xs ++ dropWhile p xs = xs</hask>, which is not true when <hask>p = const undefined</hask> and <hask>xs /= []</hask>, as the left hand side of the equality would hence become <hask>undefined</hask>. | Another example (courtesy of Tillmann Rendel) is <hask>takeWhile p xs ++ dropWhile p xs = xs</hask>, which is not true when <hask>p = const undefined</hask> and <hask>xs /= []</hask>, as the left hand side of the equality would hence become <hask>undefined</hask>. | ||

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 however 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. | 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 however 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. |

## Revision as of 15:30, 20 April 2011

DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.

## Contents |

## 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. 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#Caveats for details.

- Its property language is a Haskell DSL, so should be relatively intuitive.

## 2 Example Usage

The first thing you need is the `Zeno.hs` file, this should be in Zeno's installation directory, or you can grab it [here]. This contains the definitions for Haskell's property DSL so now we can start writing our code:

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

`Zeno.hs`will import for you. Now that we have some code we can define a property about this code. Properties are built through equality between terms, using the

`Zeno.hs`. We then pass this to the

`Zeno.hs`file to see how properties are constructed (it's very short).

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

`zeno Test.hs`. As a bug/feature this will also check

`Zeno.hs`, as this looks like a property. To restrict this to just

`zeno -m prop Test.hs`, which will only check properties whose name contains the text

`prop`. Say we want to express arbitrary propositions, we can do an equality check with

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

Here

## 3 Caveats

### 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.

While the above restrictions are founded in Isabelle's input language, there are a few which are laziness on part of Zeno's developers, and are on our to-do list:

- No partial definitions; only use total pattern matches.
- No mututally recursive datatypes.
- No tuple types beyond quadruples.

If you are wondering why a certain bit of code cannot be converted to Isabelle try running Zeno with the `--print-core` flag, to output Zeno's internal representation for your code.

### 3.2 Primitive Types

Zeno can only reason about inductive datatypes, meaning the only built-in types it can use are lists, tuples and

### 3.3 Infinite and undefined values

When 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 proveYou 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 however 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.