Personal tools

Zeno

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m
(Added categories "How to" and "Tools")
 
(23 intermediate revisions by one user not shown)
Line 1: Line 1:
DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.
 
 
 
== Introduction ==
 
== 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.
+
[http://hackage.haskell.org/package/zeno Zeno] is an automated proof system for Haskell program properties; developed at Imperial College London by William Sonnex, [http://www.doc.ic.ac.uk/~scd/ Sophia Drossopoulou] and [http://www.doc.ic.ac.uk/~susan/ 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 [http://en.wikipedia.org/wiki/Structural_induction inductively] prove properties over an infinite search space, but only those with a small and simple specification.
 
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 [http://en.wikipedia.org/wiki/Structural_induction inductively] prove properties over an infinite search space, but only those with a small and simple specification.
   
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno TryZeno], or <tt>cabal install zeno</tt> to use it from home. Find the latest paper on Zeno [http://pubs.doc.ic.ac.uk/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.
+
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno TryZeno], or <tt>cabal install zeno</tt> to use it from home. You can find the latest paper on Zeno [http://pubs.doc.ic.ac.uk/zenoTwo/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.
 
   
 
=== Features ===
 
=== Features ===
   
* 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 [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle/HOL] theory file and will automatically invoke 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#Caveats]] for details.
+
* 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.
   
* Its property language is a Haskell DSL, so should be relatively intuitive.
+
* Has a built-in counter-example finder, along the same lines as [http://www.cs.york.ac.uk/fp/smallcheck/ SmallCheck], but using symbolic evaluation to control search depth.
   
  +
* Its property language is just a Haskell DSL.
   
 
== Example Usage ==
 
== Example Usage ==
   
The first thing you need is the <tt>Zeno.hs</tt> 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:
+
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Zeno's property DSL. It should be in your Zeno installation directory but is also given below:
  +
  +
<haskell>
  +
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)
  +
</haskell>
  +
  +
  +
Making sure this file is in the same directory we can now start coding:
   
 
<haskell>
 
<haskell>
Line 46: Line 45:
 
</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 Haskell types we have are lists, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.
+
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 and tuples, 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. Equality is expressed 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>).
   
 
The following code will express that the length of two appended lists is the sum of their individual lengths:
 
The following code will express that the length of two appended lists is the sum of their individual lengths:
Line 59: Line 58:
 
Add this to the above code and save it to <tt>Test.hs</tt>. We can now check <hask>prop_length</hask> by running <tt>zeno Test.hs</tt>. As a bug/feature this will also check <hask>Zeno.proveBool</hask>, a helper function in <tt>Zeno.hs</tt>, as this looks like a property. To restrict this to just <hask>prop_length</hask> we can run <tt>zeno -m prop Test.hs</tt>, which will only check properties whose name contains the text <tt>prop</tt>.
 
Add this to the above code and save it to <tt>Test.hs</tt>. We can now check <hask>prop_length</hask> by running <tt>zeno Test.hs</tt>. As a bug/feature this will also check <hask>Zeno.proveBool</hask>, a helper function in <tt>Zeno.hs</tt>, as this looks like a property. To restrict this to just <hask>prop_length</hask> we can run <tt>zeno -m prop Test.hs</tt>, which will only check properties whose name contains the text <tt>prop</tt>.
   
Say we want to express arbitrary propositions, we can do an equality check with <hask>True</hask>. Take the following code (appended to the code above):
+
Say we want to express arbitrary propositions, we can do an equality check with <hask>True</hask>, as in the following code (appended to the code above):
   
 
<haskell>
 
<haskell>
Line 74: Line 73:
 
</haskell><br/>
 
</haskell><br/>
   
We have also provided the helper function <hask>proveBool</hask> to make this more succinct; an equivalent definition of <hask>prop_eq_ref</hask> would be:
+
We have provided the helper function <hask>proveBool</hask> to make this more succinct; an equivalent definition of <hask>prop_eq_ref</hask> would be:
 
 
 
<haskell>
 
<haskell>
Line 95: Line 94:
 
</haskell><br/>
 
</haskell><br/>
   
Here <hask>prop_elem</hask> expresses that if <hask>n</hask> is an element of <hask>ys</hask> then <hask>n</hask> is an element of <hask>xs ++ ys</hask>. Notice that we had to explicitly type everything to be <hask>Nat</hask>, as this proof does not exist for every type (consider the <hask>()</hask> type).
+
Here <hask>prop_elem</hask> expresses that if <hask>n</hask> is an element of <hask>ys</hask> then <hask>n</hask> is an element of <hask>xs ++ ys</hask>. Notice that we had to explicitly type everything to be <hask>Nat</hask> so as to give Zeno an explicit definition for <hask>(==)</hask>.
   
+
== Limitations ==
== Caveats ==
 
   
 
=== Isabelle/HOL output ===
 
=== Isabelle/HOL output ===
Line 104: Line 103:
   
 
# No internal recursive definitions; don't put recursive functions inside your functions.
 
# 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.
+
# 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 laziness on part of Zeno's developers, and are on our to-do list:
+
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 partial definitions; only use total pattern matches.
Line 113: Line 112:
 
# 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.
 
# 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 <tt>--print-core</tt> flag, to output Zeno's internal representation for your code.
+
If you are wondering why a certain bit of code cannot be converted to Isabelle try running Zeno with the <tt>--print-core</tt> flag, this will output Zeno's internal representation for your code.
 
   
 
=== Primitive Types ===
 
=== Primitive Types ===
   
Zeno can only reason about inductive datatypes, meaning the only built-in types it can use are lists, tuples and <hask>Bool</hask>s. No <hask>Integer</hask>s, <hask>Int</hask>s, <hask>Char</hask>s, etc.; Zeno will replace them all with <hask>undefined</hask>.
+
Zeno can only reason about inductive datatypes, meaning the only built-in types it can use are lists, tuples and <hask>Bool</hask>. Any values of type <hask>Integer</hask>, <hask>Int</hask>, <hask>Char</hask>, etc. Zeno will replace with <hask>undefined</hask>.
 
   
 
=== Infinite and undefined values ===
 
=== Infinite and undefined values ===
Line 123: Line 122:
 
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>).
 
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 Zeno will prove but in fact is not true when <hask>p = const undefined</hask> and <hask>xs /= []</hask>, as the left hand side of the equality would be <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 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 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.
  +
  +
[[Category:How to]]
  +
[[Category:Tools]]

Latest revision as of 15:52, 22 February 2012

Contents

[edit] 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.

[edit] 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.

[edit] 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
Prelude
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 and tuples, which are automatically available, and
Bool
, which Zeno.hs will import for you. Now that we have some code we can define a property about this code. Equality is expressed using the
(:=:)
constructor defined in Zeno.hs. We then pass this to the
prove
function to turn an equality into a property (
Prop
).

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
prop_length
by running zeno Test.hs. As a bug/feature this will also check
Zeno.proveBool
, a helper function in Zeno.hs, as this looks like a property. To restrict this to just
prop_length
we can run 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
True
, as in the following code (appended to the code above):
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
proveBool
to make this more succinct; an equivalent definition of
prop_eq_ref
would be:
prop_eq_ref x = proveBool (x == x)

We can also express implication in our properties, using the
given
and
givenBool
functions:
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
prop_elem
expresses that if
n
is an element of
ys
then
n
is an element of
xs ++ ys
. Notice that we had to explicitly type everything to be
Nat
so as to give Zeno an explicit definition for
(==)
.

[edit] 3 Limitations

[edit] 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:

  1. No internal recursive definitions; don't put recursive functions inside your functions.
  2. 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:

  1. No partial definitions; only use total pattern matches.
  2. No mututally recursive datatypes.
  3. No tuple types beyond quadruples.
  4. 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.

[edit] 3.2 Primitive Types

Zeno can only reason about inductive datatypes, meaning the only built-in types it can use are lists, tuples and
Bool
. Any values of type
Integer
,
Int
,
Char
, etc. Zeno will replace with
undefined
.

[edit] 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 prove
reverse (reverse xs) = xs
, which is not true for infinite lists, as
xs
could still be pattern matched upon, whereas evaluating
reverse (reverse xs)
starts an infinite loop (
undefined
). Another example (courtesy of Tillmann Rendel) is
takeWhile p xs ++ dropWhile p xs = xs
, which Zeno will prove but in fact is not true when
p = const undefined
and
xs /= []
, as the left hand side of the equality would be
undefined
.

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.