https://wiki.haskell.org/api.php?action=feedcontributions&user=Will&feedformat=atomHaskellWiki - User contributions [en]2020-02-28T22:40:31ZUser contributionsMediaWiki 1.27.4https://wiki.haskell.org/index.php?title=Zeno&diff=44603Zeno2012-02-22T15:40:58Z<p>Will: Updated the latest Zeno paper</p>
<hr />
<div>== Introduction ==<br />
<br />
[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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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> so as to give Zeno an explicit definition for <hask>(==)</hask>.<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# 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.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=40066Zeno2011-05-20T12:32:56Z<p>Will: /* Example Usage */</p>
<hr />
<div>== Introduction ==<br />
<br />
[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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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> so as to give Zeno an explicit definition for <hask>(==)</hask>.<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# 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.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39709Zeno2011-04-28T18:55:19Z<p>Will: Released!</p>
<hr />
<div>== Introduction ==<br />
<br />
[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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# 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.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39672Zeno2011-04-26T15:56:08Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno2 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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# 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.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39638Zeno2011-04-22T14:30:11Z<p>Will: /* Isabelle/HOL output */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno2 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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# 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.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39637Zeno2011-04-22T12:38:44Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno2 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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39636Zeno2011-04-22T12:19:40Z<p>Will: /* Introduction */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
One can try Zeno online at [http://www.doc.ic.ac.uk/~ws506/tryzeno2 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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
{-# LANGUAGE ExistentialQuantification #-}<br />
<br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39614Zeno2011-04-20T19:12:08Z<p>Will: /* Features */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
{-# LANGUAGE ExistentialQuantification #-}<br />
<br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39613Zeno2011-04-20T19:10:08Z<p>Will: /* Introduction */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
{-# LANGUAGE ExistentialQuantification #-}<br />
<br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39612Zeno2011-04-20T19:09:57Z<p>Will: Fully listed Zeno.hs</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
The first thing you need is the <tt>Zeno.hs</tt> file which contains the definitions for Haskell's property DSL. It should be in your Zeno installation directory but is also given below:<br />
<br />
<haskell><br />
{-# LANGUAGE ExistentialQuantification #-}<br />
<br />
module Zeno (<br />
Bool (..), Equals (..), Prop,<br />
prove, proveBool, given, givenBool,<br />
($), otherwise<br />
) where<br />
<br />
import Prelude ( Bool (..) )<br />
<br />
infix 1 :=:<br />
infixr 0 $<br />
<br />
($) :: (a -> b) -> a -> b<br />
f $ x = f x<br />
<br />
otherwise :: Bool<br />
otherwise = True<br />
<br />
data Equals<br />
= forall a . (:=:) a a<br />
<br />
data Prop<br />
= Given Equals Prop <br />
| Prove Equals<br />
<br />
prove :: Equals -> Prop<br />
prove = Prove<br />
<br />
given :: Equals -> Prop -> Prop<br />
given = Given<br />
<br />
proveBool :: Bool -> Prop<br />
proveBool p = Prove (p :=: True)<br />
<br />
givenBool :: Bool -> Prop -> Prop<br />
givenBool p = Given (p :=: True)<br />
</haskell><br />
<br />
<br />
Making sure this file is in the same directory we can now start coding:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39611Zeno2011-04-20T19:03:50Z<p>Will: /* Introduction */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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/zeno/ here], though please note that Zeno no longer uses the described proof output syntax but instead outputs proofs as Isabelle theories.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39610Zeno2011-04-20T19:03:15Z<p>Will: /* Isabelle/HOL output */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39609Zeno2011-04-20T18:10:05Z<p>Will: /* Features */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is just a Haskell DSL.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39608Zeno2011-04-20T18:09:24Z<p>Will: /* Primitive Types */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39607Zeno2011-04-20T18:07:52Z<p>Will: /* Introduction */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39606Zeno2011-04-20T18:04:55Z<p>Will: /* Infinite and undefined values */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39605Zeno2011-04-20T18:02:50Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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>). It is highly recommended to look at the <tt>Zeno.hs</tt> file to see how properties are constructed (it's very short).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39604Zeno2011-04-20T18:01:52Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<br />
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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39603Zeno2011-04-20T18:00:00Z<p>Will: /* Features */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39602Zeno2011-04-20T17:56:02Z<p>Will: /* Isabelle/HOL output */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39601Zeno2011-04-20T17:55:27Z<p>Will: </p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Limitations ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39600Zeno2011-04-20T17:54:00Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you.<br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39599Zeno2011-04-20T17:53:09Z<p>Will: /* Example Usage */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 and tuples, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you. <br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39598Zeno2011-04-20T17:51:45Z<p>Will: </p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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. <br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
# 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.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Applications_and_libraries/Theorem_provers&diff=39589Applications and libraries/Theorem provers2011-04-20T15:31:22Z<p>Will: /* Applications */</p>
<hr />
<div>Tools for formal reasoning, written in Haskell.<br />
<br />
== Applications ==<br />
<br />
;[http://wiki.portal.chalmers.se/agda/agda.php Agda] <br />
:Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with [[Dependent type]]s. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.<br />
<br />
;[http://citeseer.ist.psu.edu/29367.html A resolution-based theorem prover for FOL]<br />
:Haskell implementation of a resolution based theorem prover for first order logic.<br />
<br />
;[http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi Automatic generation of free theorems]<br />
:Web interface for generating theorems from Haskell types.<br />
<br />
;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila]<br />
:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page.<br />
<br />
;[http://web.archive.org/web/20080524225132/http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne]<br />
:Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system. The language is no longer supportd; the link points to a page stored in the Web Archive.<br />
<br />
;[http://www.lix.polytechnique.fr/dedukti Dedukti]<br />
:Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo.<br />
<br />
;[http://www.cwi.nl/~jve/demo/ DEMO]<br />
:Model checking for dynamic epistemic logic. DEMO is a tool for modelling change in epistemic logic (the logic of knowledge). Among other things, DEMO allows modeling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL (propositional dynamic logic) formulas. More materials and other Haskell resources on dynamic epistemic modelling (and more generally on logic and [[linguistics]]) can be found on [http://homepages.cwi.nl/~jve/index.html Jan van Eijck's page].<br />
;[http://darcs.augustsson.net/Darcs/Djinn Djinn]<br />
:Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.<br />
<br />
;[http://www.haskell.org/dumatel/ Dumatel] <br />
: Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning<br />
<br />
;[http://www.e-pig.org/ Epigram]<br />
:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.<br />
<br />
;[http://www.cs.chalmers.se/~koen/folkung/ Equinox]<br />
:Equinox is a new theorem prover for pure first-order logic with equality. It finds ground proofs of the input theory, by solving successive ground instantiations of the theory using an incremental SAT-solver. Equality is dealt with using a Nelson-Oppen framework.<br />
<br />
;[http://fldit-www.cs.uni-dortmund.de/~peter/ExpNeu/Welcome.html Expander2]<br />
:Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures.<br />
<br />
;[http://www.cs.yale.edu/homes/cc392/report.html FOL Resolution Theorem Prover]<br />
:An implementation of a simple theorem prover in first-order logic using Haskell.<br />
<br />
;[http://taz.cs.wcupa.edu/~dmead/code/prover/ Halp]<br />
:Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written with gtk2hs<br />
<br />
;[http://isabelle.in.tum.de/haskabelle.html Haskabelle]<br />
:Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself<br />
<br />
;[http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/ Hets]<br />
:The Heterogeneous Tool Set (Hets) is a parsing, static analysis and proof management tool combining various tools for different specification languages, thus providing a tool for heterogeneous specifications. It supports HasCASL for specification of Haskell programs, and uses Isabelle for proving<br />
<br />
;[http://www.math.chalmers.se/~koen/paradox/ Paradox]<br />
:Paradox processes first-order logic problems and tries to find finite-domain models for them.<br />
<br />
;[http://proofgeneral.inf.ed.ac.uk/Kit Proof General Kit]<br />
:The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface.<br />
<br />
;[http://www.haskell.org/yarrow/ Yarrow]<br />
:Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages.<br />
<br />
;[[Zeno]]<br />
: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. Proofs and programs are output as [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle/HOL] theories which are then automatically verified by said tool.<br />
<br />
== Libraries ==<br />
<br />
;[http://www.dcs.st-and.ac.uk/~eb/ivor.php Ivor]<br />
:is type theory based theorem proving library -- written by [http://www.dcs.st-and.ac.uk/~eb/index.php Edwin Brady] (see also the author's homepage, there are a lot of materials concerning [[dependent type]] theory there).<br />
<br />
{{LibrariesPage}}</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39588Zeno2011-04-20T15:30:47Z<p>Will: /* Infinite and undefined values */</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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. <br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39587Zeno2011-04-20T15:30:20Z<p>Will: </p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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. <br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also express implication in our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Applications_and_libraries/Theorem_provers&diff=39586Applications and libraries/Theorem provers2011-04-20T15:28:44Z<p>Will: forgot a bracket</p>
<hr />
<div>Tools for formal reasoning, written in Haskell.<br />
<br />
== Applications ==<br />
<br />
;[http://wiki.portal.chalmers.se/agda/agda.php Agda] <br />
:Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with [[Dependent type]]s. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.<br />
<br />
;[http://citeseer.ist.psu.edu/29367.html A resolution-based theorem prover for FOL]<br />
:Haskell implementation of a resolution based theorem prover for first order logic.<br />
<br />
;[http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi Automatic generation of free theorems]<br />
:Web interface for generating theorems from Haskell types.<br />
<br />
;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila]<br />
:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page.<br />
<br />
;[http://web.archive.org/web/20080524225132/http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne]<br />
:Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system. The language is no longer supportd; the link points to a page stored in the Web Archive.<br />
<br />
;[http://www.lix.polytechnique.fr/dedukti Dedukti]<br />
:Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo.<br />
<br />
;[http://www.cwi.nl/~jve/demo/ DEMO]<br />
:Model checking for dynamic epistemic logic. DEMO is a tool for modelling change in epistemic logic (the logic of knowledge). Among other things, DEMO allows modeling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL (propositional dynamic logic) formulas. More materials and other Haskell resources on dynamic epistemic modelling (and more generally on logic and [[linguistics]]) can be found on [http://homepages.cwi.nl/~jve/index.html Jan van Eijck's page].<br />
;[http://darcs.augustsson.net/Darcs/Djinn Djinn]<br />
:Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.<br />
<br />
;[http://www.haskell.org/dumatel/ Dumatel] <br />
: Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning<br />
<br />
;[http://www.e-pig.org/ Epigram]<br />
:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.<br />
<br />
;[http://www.cs.chalmers.se/~koen/folkung/ Equinox]<br />
:Equinox is a new theorem prover for pure first-order logic with equality. It finds ground proofs of the input theory, by solving successive ground instantiations of the theory using an incremental SAT-solver. Equality is dealt with using a Nelson-Oppen framework.<br />
<br />
;[http://fldit-www.cs.uni-dortmund.de/~peter/ExpNeu/Welcome.html Expander2]<br />
:Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures.<br />
<br />
;[http://www.cs.yale.edu/homes/cc392/report.html FOL Resolution Theorem Prover]<br />
:An implementation of a simple theorem prover in first-order logic using Haskell.<br />
<br />
;[http://taz.cs.wcupa.edu/~dmead/code/prover/ Halp]<br />
:Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written with gtk2hs<br />
<br />
;[http://isabelle.in.tum.de/haskabelle.html Haskabelle]<br />
:Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself<br />
<br />
;[http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/ Hets]<br />
:The Heterogeneous Tool Set (Hets) is a parsing, static analysis and proof management tool combining various tools for different specification languages, thus providing a tool for heterogeneous specifications. It supports HasCASL for specification of Haskell programs, and uses Isabelle for proving<br />
<br />
;[http://www.math.chalmers.se/~koen/paradox/ Paradox]<br />
:Paradox processes first-order logic problems and tries to find finite-domain models for them.<br />
<br />
;[http://proofgeneral.inf.ed.ac.uk/Kit Proof General Kit]<br />
:The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface.<br />
<br />
;[http://www.haskell.org/yarrow/ Yarrow]<br />
:Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages.<br />
<br />
;[[Zeno]]<br />
: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. Proofs are output as [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle/HOL] theories which are then automatically verified by said tool.<br />
<br />
== Libraries ==<br />
<br />
;[http://www.dcs.st-and.ac.uk/~eb/ivor.php Ivor]<br />
:is type theory based theorem proving library -- written by [http://www.dcs.st-and.ac.uk/~eb/index.php Edwin Brady] (see also the author's homepage, there are a lot of materials concerning [[dependent type]] theory there).<br />
<br />
{{LibrariesPage}}</div>Willhttps://wiki.haskell.org/index.php?title=Applications_and_libraries/Theorem_provers&diff=39585Applications and libraries/Theorem provers2011-04-20T15:28:24Z<p>Will: Updated the Zeno entry</p>
<hr />
<div>Tools for formal reasoning, written in Haskell.<br />
<br />
== Applications ==<br />
<br />
;[http://wiki.portal.chalmers.se/agda/agda.php Agda] <br />
:Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with [[Dependent type]]s. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.<br />
<br />
;[http://citeseer.ist.psu.edu/29367.html A resolution-based theorem prover for FOL]<br />
:Haskell implementation of a resolution based theorem prover for first order logic.<br />
<br />
;[http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi Automatic generation of free theorems]<br />
:Web interface for generating theorems from Haskell types.<br />
<br />
;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila]<br />
:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page.<br />
<br />
;[http://web.archive.org/web/20080524225132/http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne]<br />
:Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system. The language is no longer supportd; the link points to a page stored in the Web Archive.<br />
<br />
;[http://www.lix.polytechnique.fr/dedukti Dedukti]<br />
:Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo.<br />
<br />
;[http://www.cwi.nl/~jve/demo/ DEMO]<br />
:Model checking for dynamic epistemic logic. DEMO is a tool for modelling change in epistemic logic (the logic of knowledge). Among other things, DEMO allows modeling epistemic updates, graphical display of update results, graphical display of action models, formula evaluation in epistemic models, translation of dynamic epistemic formulas to PDL (propositional dynamic logic) formulas. More materials and other Haskell resources on dynamic epistemic modelling (and more generally on logic and [[linguistics]]) can be found on [http://homepages.cwi.nl/~jve/index.html Jan van Eijck's page].<br />
;[http://darcs.augustsson.net/Darcs/Djinn Djinn]<br />
:Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.<br />
<br />
;[http://www.haskell.org/dumatel/ Dumatel] <br />
: Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning<br />
<br />
;[http://www.e-pig.org/ Epigram]<br />
:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.<br />
<br />
;[http://www.cs.chalmers.se/~koen/folkung/ Equinox]<br />
:Equinox is a new theorem prover for pure first-order logic with equality. It finds ground proofs of the input theory, by solving successive ground instantiations of the theory using an incremental SAT-solver. Equality is dealt with using a Nelson-Oppen framework.<br />
<br />
;[http://fldit-www.cs.uni-dortmund.de/~peter/ExpNeu/Welcome.html Expander2]<br />
:Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures.<br />
<br />
;[http://www.cs.yale.edu/homes/cc392/report.html FOL Resolution Theorem Prover]<br />
:An implementation of a simple theorem prover in first-order logic using Haskell.<br />
<br />
;[http://taz.cs.wcupa.edu/~dmead/code/prover/ Halp]<br />
:Haskell Logic Prover is written in Haskell supports first order logic with plans to add predicates. Also included is a simple frontend written with gtk2hs<br />
<br />
;[http://isabelle.in.tum.de/haskabelle.html Haskabelle]<br />
:Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself<br />
<br />
;[http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/ Hets]<br />
:The Heterogeneous Tool Set (Hets) is a parsing, static analysis and proof management tool combining various tools for different specification languages, thus providing a tool for heterogeneous specifications. It supports HasCASL for specification of Haskell programs, and uses Isabelle for proving<br />
<br />
;[http://www.math.chalmers.se/~koen/paradox/ Paradox]<br />
:Paradox processes first-order logic problems and tries to find finite-domain models for them.<br />
<br />
;[http://proofgeneral.inf.ed.ac.uk/Kit Proof General Kit]<br />
:The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface.<br />
<br />
;[http://www.haskell.org/yarrow/ Yarrow]<br />
:Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages.<br />
<br />
;[[Zeno]<br />
: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. Proofs are output as [http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Isabelle/HOL] theories which are then automatically verified by said tool.<br />
<br />
== Libraries ==<br />
<br />
;[http://www.dcs.st-and.ac.uk/~eb/ivor.php Ivor]<br />
:is type theory based theorem proving library -- written by [http://www.dcs.st-and.ac.uk/~eb/index.php Edwin Brady] (see also the author's homepage, there are a lot of materials concerning [[dependent type]] theory there).<br />
<br />
{{LibrariesPage}}</div>Willhttps://wiki.haskell.org/index.php?title=Zeno&diff=39570Zeno2011-04-20T14:43:40Z<p>Will: Created the wiki page for Zeno.</p>
<hr />
<div>DRAFT. THE VERSION OF ZENO DESCRIBED HEREIN HAS NOT YET BEEN RELEASED.<br />
<br />
== Introduction ==<br />
<br />
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.<br />
<br />
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.<br />
<br />
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.<br />
<br />
<br />
=== Features ===<br />
<br />
* 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).<br />
<br />
* 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 Caveats]] for details.<br />
<br />
* Its property language is a Haskell DSL, so should be relatively intuitive.<br />
<br />
<br />
== Example Usage ==<br />
<br />
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:<br />
<br />
<haskell><br />
module Test where<br />
<br />
import Prelude ()<br />
import Zeno<br />
<br />
data Nat = Zero | Succ Nat<br />
<br />
length :: [a] -> Nat<br />
length [] = Zero<br />
length (x:xs) = Succ (length xs)<br />
<br />
(++) :: [a] -> [a] -> [a]<br />
[] ++ ys = ys<br />
(x:xs) ++ ys = x : (xs ++ ys)<br />
<br />
class Num a where<br />
(+) :: a -> a -> a<br />
<br />
instance Num Nat where<br />
Zero + y = y<br />
Succ x + y = Succ (x + y)<br />
</haskell><br/><br />
<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 GHC types we have are lists, which are automatically available, and <hask>Bool</hask>, which <tt>Zeno.hs</tt> will import for you. <br />
<br />
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).<br />
<br />
The following code will express that the length of two appended lists is the sum of their individual lengths:<br />
<br />
<haskell><br />
prop_length xs ys<br />
= prove (length (xs ++ ys) :=: length xs + length ys)<br />
</haskell><br/><br />
<br />
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>.<br />
<br />
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):<br />
<br />
<haskell><br />
class Eq a where<br />
(==) :: a -> a -> Bool<br />
<br />
instance Eq Nat where<br />
Zero == Zero = True<br />
Succ x == Succ y = x == y<br />
_ == _ = False<br />
<br />
prop_eq_ref :: Nat -> Prop<br />
prop_eq_ref x = prove (x == x :=: True)<br />
</haskell><br/><br />
<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:<br />
<br />
<haskell><br />
prop_eq_ref x = proveBool (x == x)<br />
</haskell><br/><br />
<br />
We can also add conditions/antecedents to our properties, using the <hask>given</hask> and <hask>givenBool</hask> functions:<br />
<br />
<haskell><br />
elem :: Eq a => a -> [a] -> Bool<br />
elem _ [] = False<br />
elem n (x:xs) <br />
| n == x = True<br />
| otherwise = elem n xs<br />
<br />
prop_elem :: Nat -> [Nat] -> [Nat] -> Prop<br />
prop_elem n xs ys<br />
= givenBool (n `elem` ys)<br />
$ proveBool (n `elem` (xs ++ ys))<br />
</haskell><br/><br />
<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).<br />
<br />
<br />
== Caveats ==<br />
<br />
=== Isabelle/HOL output ===<br />
<br />
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:<br />
<br />
# No internal recursive definitions; don't put recursive functions inside your functions.<br />
# No non-terminating definitions. This also means you cannot use default type-class methods, as GHC transforms these internally to a co-recursive value.<br />
<br />
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:<br />
<br />
# No partial definitions; only use total pattern matches.<br />
# No mututally recursive datatypes.<br />
# No tuple types beyond quadruples.<br />
<br />
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.<br />
<br />
<br />
=== Primitive Types ===<br />
<br />
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>.<br />
<br />
<br />
=== Infinite and undefined values ===<br />
<br />
Everything you have just read about Zeno is a huge lie. Zeno doesn't actually prove properties of Haskell programs, but only those in 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>).<br />
<br />
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>.<br />
<br />
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.</div>Willhttps://wiki.haskell.org/index.php?title=Template:Zeno_infobox&diff=39534Template:Zeno infobox2011-04-20T11:11:07Z<p>Will: New page: Zeno</p>
<hr />
<div>Zeno</div>Willhttps://wiki.haskell.org/index.php?title=AngloHaskell/2010&diff=36776AngloHaskell/20102010-09-15T13:45:11Z<p>Will: </p>
<hr />
<div>AngloHaskell 2010 is taking place on the 10th and 11th of September in Cambridge, UK (yes, tradition has been broken and month has changed!). It's free, and everyone is invited! Simply add your name to the wiki and we'll see you there.<br />
<br />
Organisational contact: Derek Wright (07857 984 549)<br />
<br />
== Dates and Venues ==<br />
<br />
{| class="wikitable"<br />
|-<br />
! Date !! Venue<br />
|-<br />
| Friday 10th September || Microsoft Research, Cambridge, UK<br />
|-<br />
| Saturday 11th September || [http://www.jdwetherspoon.co.uk/home/pubs/the-regal The Regal] Wetherspoons pub with Wi-Fi (Any better suggestions?)<br />
|}<br />
<br />
== Attendees ==<br />
<br />
Per last year, all attendees should '''bring or make a nametag''' that identifies you by your real name and/or IRC name. If anyone wants to drag a roll of stickers and a pen along that'll help!<br />
<br />
If you can't make the start on Friday, or can only make it on Saturday, that's fine. If you're not sure where everyone's going to be, give one of the contacts a call or a text (Derek Wright = 07857 984 549)<br />
<br />
=== Definite ===<br />
<br />
* Derek Wright (Fri + Sat) [WiFi]<br />
* Graeme Burnett (Fri + Sat)<br />
* Sam Martin (Fri but not Sat)<br />
* Eric Kow (Fri + Sat) [WiFi]<br />
* Richard Smith (Fri only)<br />
* Benedict Eastaugh (Fri only) [WiFi]<br />
* Simon Marlow (Fri only)<br />
* Tristan Allwood (Fri only) [WiFi]<br />
* Tony Cowderoy (Fri + Sat)<br />
* Philippa Cowderoy (Fri + Sat) [WiFi]<br />
* Will Sonnex (Fri) [WiFi]<br />
* Miëtek Bak (Fri) [WiFi]<br />
* Will Jones (Fri)<br />
* Claude Heiland-Allen (Fri)<br />
* Alex McLean (Fri, can't do Sat) [WiFi]<br />
* Pedro Martins (Fri) [WiFi]<br />
* Nik Sultana (Fri + Sat)<br />
* Rob Henderson (just Friday)<br />
* Pasqualino "Titto" Assini (Fri + Sat)<br />
* Sam Aaron (Fri)<br />
* Max Bolingbroke (Fri)<br />
<br />
* Add your name here<br />
<br />
=== Possible ===<br />
<br />
* Joshua Lee Tucker<br />
* Ben May<br />
* Richard Fergie (just Friday)<br />
* Roland Swingler<br />
* Vincent Hanquez<br />
* Louis Zhuang (hopefully Sat)<br />
* Thomas Schilling (Fri only)<br />
* Neil Mitchell (hopefully Sat)<br />
* Add your name here<br />
<br />
=== Not this year, but hopefully next! ===<br />
<br />
* Ganesh Sittampalam<br />
* Magnus Therning (Fri) [WiFi]<br />
<br />
=== Wifi Signup ===<br />
<br />
Wifi accounts are available on request. The signup deadline is Wednesday 8th September. Everyone wanting an account should provide:<br />
<br />
* Full name<br />
* Institution<br />
* Country of Residence<br />
* Email Address<br />
<br />
Signups here: <br />
<br />
If you'd prefer not to give details here, please email derek at obvious dot co dot uk with the subject "AngloHaskell Wifi Signup".<br />
<br />
* Derek Wright, Obvious Limited, UK, derek at obvious dot co dot uk<br />
* Philippa Cowderoy, , UK, flippa at flippac dot org<br />
* Tristan Allwood, Imperial College, UK, tora at doc dot ic dot ac dot uk<br />
* Will Sonnex, Imperial College, UK, will at sonnex dot name<br />
* Pedro Martins, Imperial College, UK, pedromartins dot pt at gmail dot com<br />
* Add Full Name, Institution, Country of Residence, Email Address<br />
<br />
== Lodging ==<br />
<br />
It's likely that there'll be people in need of crashspace and so forth, so please organise here! Both offers and requests are good.<br />
<br />
=== Hostels ===<br />
<br />
Details coming soon...<br />
<br />
== Programme ==<br />
<br />
Planning will be taking place on IRC as per previous years: #anglohaskell on irc.freenode.net<br />
<br />
If you're having trouble following things on IRC, the discussion page on the wiki might be a good place to leave comments and questions.<br />
<br />
In previous years we had talks in the day on a Friday, followed by pubbage in the evening and assorted activities on the Saturday. This seemed to work, so we'll follow a similar model this year.<br />
<br />
=== Timetable ===<br />
<br />
This is somewhat preliminary and subject to change as talks are confirmed or otherwise, but the overall structure should hold: <br />
<br />
{| class="wikitable"<br />
|-<br />
! Day !! Time !! Event<br />
|-<br />
| Friday or Saturday || 10am || People start arriving<br />
|-<br />
| || 10:30 am || Tea, coffee and biscuits<br />
|-<br />
| || 11am - Welcome / Talks || Simon Peyton Jones: Welcome to Microsoft Research Cambridge & AngloHaskell<br />
|-<br />
| || || Simon Marlow: Scheduling lazy evaluation on multicore<br />
|-<br />
| || || Claude Heiland-Allen: mandulia - A zooming visualisation of the Mandelbrot Set as many Julia Sets<br />
|-<br />
| || 12-15pm || Lunch<br />
|-<br />
| || 1-15pm - More talks || Alex McLean: tidal - live coding patterns with Haskell<br />
|-<br />
| || || Will Sonnex: Zeno - automated proofs of Haskell programs<br />
|-<br />
| || || Pasqualino "Titto" Assini: QuidQuid - using Haskell to Turn the Internet on its Head<br />
|-<br />
| || 3pm || Tea, coffee and biscuits<br />
|-<br />
| || 3-30pm - Remaining talks || Eric Kow: Darcs in 2010<br />
|-<br />
| || Then || Functional Grit - small talks that may grow into functional pearls. Open session, anyone can give a quick talk!<br />
|-<br />
| || When people get hungry or the venue kicks us out || Food! Likely we'll head out for a curry<br />
|-<br />
| || Beer o'Clock || When everyone's finished eating, we'll head for a nearby pub<br />
|-<br />
| 2nd Day || From 10am-ish || [http://www.jdwetherspoon.co.uk/home/pubs/the-regal The Regal]<br />
<br />
Wetherspoons pub with Wi-Fi near the centre of town ( [http://maps.google.co.uk/maps/place?cid=4630934221894119690 Google Map] )<br />
|}<br />
<br />
=== Talks ===<br />
<br />
Volunteers please! Previously we have had a largely more practical set of talks than you might find at Fun in the Afternoon or an academic event. This was a good thing, and some of the best talks were from people who were far from considering themselves as experts, so feel free to tell us about your experiences.<br />
<br />
Talks planned and/or offered:<br />
<br />
* Claude Heiland-Allen - "mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets" ([http://claudiusmaximus.goto10.org/t/hs/mandulia_anglohaskell_2010-09-10.pdf PDF])<br />
* Alex McLean - "tidal - live coding patterns with Haskell"<br />
* Simon Marlow - "Scheduling lazy evaluation on multicore"<br />
* Will Sonnex - "Zeno - automated proofs of Haskell programs" ([http://www.doc.ic.ac.uk/~ws506/tryzeno/ Try It Online!]) ([http://www.doc.ic.ac.uk/~ws506/tryzeno/pdf/presentation.pdf Slides])<br />
* Eric Kow - "[http://prezi.com/is5nzudw8jxq/darcs-in-2010/ Darcs in 2010]"<br />
* Pasqualino "Titto" Assini - "QuidQuid: using Haskell to Turn the Internet on its Head" ([http://quicquid.org/presentation/QuidQuid.ppt PowerPoint], [http://quicquid.org/presentation/QuidQuid.htm HTML], [http://quicquid.org/presentation/QuidQuid.pdf PDF])<br />
* Add your name here - Add your title here<br />
<br />
==== Abstracts ====<br />
<br />
People giving talks should add these as they have them :-)<br />
<br />
* [http://hackage.haskell.org/package/mandulia-0.4 mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets]<br />
<br />
Mandulia provides a zooming visualisation of the Mandelbrot Set as many Julia Sets. Featuring a profiled and optimized renderer, and a Lua configuration and scripting interface. <br />
<br />
<br />
* Zeno - automated proofs of Haskell programs<br />
<br />
Zeno is an inductive theorem prover for properties of Haskell functions operating on recursive datatypes. Stuff like "drop n (take m xs) = take (m - n) (drop n xs)".<br />
<br />
<br />
* Title here<br />
<br />
abstract goes here<br />
<br />
==== Functional Grit ====<br />
<br />
In previous years there has been a successful 'functional grit' section. Usually an informal session for people to briefly talk/demo works in progress, no need to pre-register, just turn up and talk. Think small stones that might turn into functional pearls. If there's time it'd be great to do again this year.<br />
<br />
=== Other activity ===<br />
<br />
After Friday's talks, food and drink would be a good idea! Curry is traditional and probably the default, but we're open to other suggestions. After that, we'll retreat to a pub for the evening.<br />
<br />
<br />
[[User:DWright|Derek Wright]] (07857 984 549)<br />
<br />
[[Category:Events]]</div>Willhttps://wiki.haskell.org/index.php?title=AngloHaskell/2010&diff=36760AngloHaskell/20102010-09-13T16:28:53Z<p>Will: </p>
<hr />
<div>AngloHaskell 2010 is taking place on the 10th and 11th of September in Cambridge, UK (yes, tradition has been broken and month has changed!). It's free, and everyone is invited! Simply add your name to the wiki and we'll see you there.<br />
<br />
Organisational contact: Derek Wright (07857 984 549)<br />
<br />
== Dates and Venues ==<br />
<br />
{| class="wikitable"<br />
|-<br />
! Date !! Venue<br />
|-<br />
| Friday 10th September || Microsoft Research, Cambridge, UK<br />
|-<br />
| Saturday 11th September || [http://www.jdwetherspoon.co.uk/home/pubs/the-regal The Regal] Wetherspoons pub with Wi-Fi (Any better suggestions?)<br />
|}<br />
<br />
== Attendees ==<br />
<br />
Per last year, all attendees should '''bring or make a nametag''' that identifies you by your real name and/or IRC name. If anyone wants to drag a roll of stickers and a pen along that'll help!<br />
<br />
If you can't make the start on Friday, or can only make it on Saturday, that's fine. If you're not sure where everyone's going to be, give one of the contacts a call or a text (Derek Wright = 07857 984 549)<br />
<br />
=== Definite ===<br />
<br />
* Derek Wright (Fri + Sat) [WiFi]<br />
* Graeme Burnett (Fri + Sat)<br />
* Sam Martin (Fri but not Sat)<br />
* Eric Kow (Fri + Sat) [WiFi]<br />
* Richard Smith (Fri only)<br />
* Benedict Eastaugh (Fri only) [WiFi]<br />
* Simon Marlow (Fri only)<br />
* Tristan Allwood (Fri only) [WiFi]<br />
* Tony Cowderoy (Fri + Sat)<br />
* Philippa Cowderoy (Fri + Sat) [WiFi]<br />
* Will Sonnex (Fri) [WiFi]<br />
* Miëtek Bak (Fri) [WiFi]<br />
* Will Jones (Fri)<br />
* Claude Heiland-Allen (Fri)<br />
* Alex McLean (Fri, can't do Sat) [WiFi]<br />
* Pedro Martins (Fri) [WiFi]<br />
* Nik Sultana (Fri + Sat)<br />
* Rob Henderson (just Friday)<br />
* Pasqualino "Titto" Assini (Fri + Sat)<br />
* Sam Aaron (Fri)<br />
* Max Bolingbroke (Fri)<br />
<br />
* Add your name here<br />
<br />
=== Possible ===<br />
<br />
* Joshua Lee Tucker<br />
* Ben May<br />
* Richard Fergie (just Friday)<br />
* Roland Swingler<br />
* Vincent Hanquez<br />
* Louis Zhuang (hopefully Sat)<br />
* Thomas Schilling (Fri only)<br />
* Neil Mitchell (hopefully Sat)<br />
* Add your name here<br />
<br />
=== Not this year, but hopefully next! ===<br />
<br />
* Ganesh Sittampalam<br />
* Magnus Therning (Fri) [WiFi]<br />
<br />
=== Wifi Signup ===<br />
<br />
Wifi accounts are available on request. The signup deadline is Wednesday 8th September. Everyone wanting an account should provide:<br />
<br />
* Full name<br />
* Institution<br />
* Country of Residence<br />
* Email Address<br />
<br />
Signups here: <br />
<br />
If you'd prefer not to give details here, please email derek at obvious dot co dot uk with the subject "AngloHaskell Wifi Signup".<br />
<br />
* Derek Wright, Obvious Limited, UK, derek at obvious dot co dot uk<br />
* Philippa Cowderoy, , UK, flippa at flippac dot org<br />
* Tristan Allwood, Imperial College, UK, tora at doc dot ic dot ac dot uk<br />
* Will Sonnex, Imperial College, UK, will at sonnex dot name<br />
* Pedro Martins, Imperial College, UK, pedromartins dot pt at gmail dot com<br />
* Add Full Name, Institution, Country of Residence, Email Address<br />
<br />
== Lodging ==<br />
<br />
It's likely that there'll be people in need of crashspace and so forth, so please organise here! Both offers and requests are good.<br />
<br />
=== Hostels ===<br />
<br />
Details coming soon...<br />
<br />
== Programme ==<br />
<br />
Planning will be taking place on IRC as per previous years: #anglohaskell on irc.freenode.net<br />
<br />
If you're having trouble following things on IRC, the discussion page on the wiki might be a good place to leave comments and questions.<br />
<br />
In previous years we had talks in the day on a Friday, followed by pubbage in the evening and assorted activities on the Saturday. This seemed to work, so we'll follow a similar model this year.<br />
<br />
=== Timetable ===<br />
<br />
This is somewhat preliminary and subject to change as talks are confirmed or otherwise, but the overall structure should hold: <br />
<br />
{| class="wikitable"<br />
|-<br />
! Day !! Time !! Event<br />
|-<br />
| Friday or Saturday || 10am || People start arriving<br />
|-<br />
| || 10:30 am || Tea, coffee and biscuits<br />
|-<br />
| || 11am - Welcome / Talks || Simon Peyton Jones: Welcome to Microsoft Research Cambridge & AngloHaskell<br />
|-<br />
| || || Simon Marlow: Scheduling lazy evaluation on multicore<br />
|-<br />
| || || Claude Heiland-Allen: mandulia - A zooming visualisation of the Mandelbrot Set as many Julia Sets<br />
|-<br />
| || 12-15pm || Lunch<br />
|-<br />
| || 1-15pm - More talks || Alex McLean: tidal - live coding patterns with Haskell<br />
|-<br />
| || || Will Sonnex: Zeno - automated proofs of Haskell programs<br />
|-<br />
| || || Pasqualino "Titto" Assini: QuidQuid - using Haskell to Turn the Internet on its Head<br />
|-<br />
| || 3pm || Tea, coffee and biscuits<br />
|-<br />
| || 3-30pm - Remaining talks || Eric Kow: Darcs in 2010<br />
|-<br />
| || Then || Functional Grit - small talks that may grow into functional pearls. Open session, anyone can give a quick talk!<br />
|-<br />
| || When people get hungry or the venue kicks us out || Food! Likely we'll head out for a curry<br />
|-<br />
| || Beer o'Clock || When everyone's finished eating, we'll head for a nearby pub<br />
|-<br />
| 2nd Day || From 10am-ish || [http://www.jdwetherspoon.co.uk/home/pubs/the-regal The Regal]<br />
<br />
Wetherspoons pub with Wi-Fi near the centre of town ( [http://maps.google.co.uk/maps/place?cid=4630934221894119690 Google Map] )<br />
|}<br />
<br />
=== Talks ===<br />
<br />
Volunteers please! Previously we have had a largely more practical set of talks than you might find at Fun in the Afternoon or an academic event. This was a good thing, and some of the best talks were from people who were far from considering themselves as experts, so feel free to tell us about your experiences.<br />
<br />
Talks planned and/or offered:<br />
<br />
* Claude Heiland-Allen - "mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets" ([http://claudiusmaximus.goto10.org/t/hs/mandulia_anglohaskell_2010-09-10.pdf PDF])<br />
* Alex McLean - "tidal - live coding patterns with Haskell"<br />
* Simon Marlow - "Scheduling lazy evaluation on multicore"<br />
* Will Sonnex - "Zeno - automated proofs of Haskell programs" ([http://www.doc.ic.ac.uk/~ws506/presentation.pdf Slides])<br />
* Eric Kow - "[http://prezi.com/is5nzudw8jxq/darcs-in-2010/ Darcs in 2010]"<br />
* Pasqualino "Titto" Assini - "QuidQuid: using Haskell to Turn the Internet on its Head" ([http://quicquid.org/presentation/QuidQuid.ppt PowerPoint], [http://quicquid.org/presentation/QuidQuid.htm HTML], [http://quicquid.org/presentation/QuidQuid.pdf PDF])<br />
* Add your name here - Add your title here<br />
<br />
==== Abstracts ====<br />
<br />
People giving talks should add these as they have them :-)<br />
<br />
* [http://hackage.haskell.org/package/mandulia-0.4 mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets]<br />
<br />
Mandulia provides a zooming visualisation of the Mandelbrot Set as many Julia Sets. Featuring a profiled and optimized renderer, and a Lua configuration and scripting interface. <br />
<br />
<br />
* Zeno - automated proofs of Haskell programs<br />
<br />
Zeno is an inductive theorem prover for properties of Haskell functions operating on recursive datatypes. Stuff like "drop n (take m xs) = take (m - n) (drop n xs)".<br />
<br />
<br />
* Title here<br />
<br />
abstract goes here<br />
<br />
==== Functional Grit ====<br />
<br />
In previous years there has been a successful 'functional grit' section. Usually an informal session for people to briefly talk/demo works in progress, no need to pre-register, just turn up and talk. Think small stones that might turn into functional pearls. If there's time it'd be great to do again this year.<br />
<br />
=== Other activity ===<br />
<br />
After Friday's talks, food and drink would be a good idea! Curry is traditional and probably the default, but we're open to other suggestions. After that, we'll retreat to a pub for the evening.<br />
<br />
<br />
[[User:DWright|Derek Wright]] (07857 984 549)<br />
<br />
[[Category:Events]]</div>Willhttps://wiki.haskell.org/index.php?title=AngloHaskell/2010&diff=36699AngloHaskell/20102010-09-07T18:27:40Z<p>Will: </p>
<hr />
<div>AngloHaskell 2010 is taking place on the 10th and 11th of September in Cambridge, UK (yes, tradition has been broken and month has changed!). It's free, and everyone is invited! Simply add your name to the wiki and we'll see you there.<br />
<br />
Organisational contact: Derek Wright<br />
<br />
== Dates and Venues ==<br />
<br />
{| class="wikitable"<br />
|-<br />
! Date !! Venue<br />
|-<br />
| Friday 10th September || Microsoft Research, Cambridge, UK<br />
|-<br />
| Saturday 11th September || A less formal venue (to be organised, any suggestions?)<br />
|}<br />
<br />
== Attendees ==<br />
<br />
Per last year, all attendees should '''bring or make a nametag''' that identifies you by your real name and/or IRC name. If anyone wants to drag a roll of stickers and a pen along that'll help!<br />
<br />
If you can't make the start on Friday, or can only make it on Saturday, that's fine. If you're not sure where everyone's going to be, give one of the contacts a call or a text.<br />
<br />
=== Definite ===<br />
<br />
* Derek Wright (Fri + Sat) [WiFi]<br />
* Graeme Burnett (Fri + Sat)<br />
* Neil Mitchell (hopefully Fri, definite Sat)<br />
* Sam Martin (Fri but not Sat)<br />
* Eric Kow (Fri + Sat) [WiFi]<br />
* Richard Smith (Fri only)<br />
* Benedict Eastaugh (Fri only) [WiFi]<br />
* Simon Marlow (Fri only)<br />
* Tristan Allwood (Fri only) [WiFi]<br />
* Magnus Therning (Fri) [WiFi]<br />
* Tony Cowderoy (Fri + Sat)<br />
* Philippa Cowderoy (Fri + Sat) [WiFi]<br />
* Will Sonnex (Fri) [WiFi]<br />
* Miëtek Bak (Fri, maybe Sat) [WiFi]<br />
* Add your name here<br />
<br />
=== Possible ===<br />
<br />
* Claude Heiland-Allen<br />
* Joshua Lee Tucker<br />
* Ben May<br />
* Alex McLean (hopefully Fri, can't do Sat)<br />
* Richard Fergie (just Friday)<br />
* Max Bolingbroke<br />
* Roland Swingler<br />
* Vincent Hanquez<br />
* Rob Henderson (just Friday)<br />
* Louis Zhuang (hopefully Sat)<br />
* Thomas Schilling (Fri only)<br />
* Add your name here<br />
<br />
=== Not this year, but hopefully next! ===<br />
<br />
* Ganesh Sittampalam<br />
<br />
=== Wifi Signup ===<br />
<br />
Wifi accounts are available on request. The signup deadline is Wednesday 8th September. Everyone wanting an account should provide:<br />
<br />
* Full name<br />
* Institution<br />
* Country of Residence<br />
* Email Address<br />
<br />
Signups here: <br />
<br />
If you'd prefer not to give details here, please email derek at obvious dot co dot uk with the subject "AngloHaskell Wifi Signup".<br />
<br />
* Derek Wright, Obvious Limited, UK, derek at obvious dot co dot uk<br />
* Philippa Cowderoy, , UK, flippa at flippac dot org<br />
* Tristan Allwood, Imperial College, UK, tora at doc dot ic dot ac dot uk<br />
* Will Sonnex, Imperial College, UK, will at sonnex dot name<br />
* Add Full Name, Institution, Country of Residence, Email Address<br />
<br />
== Lodging ==<br />
<br />
It's likely that there'll be people in need of crashspace and so forth, so please organise here! Both offers and requests are good.<br />
<br />
=== Hostels ===<br />
<br />
Details coming soon...<br />
<br />
== Programme ==<br />
<br />
Planning will be taking place on IRC as per previous years: #anglohaskell on irc.freenode.net<br />
<br />
If you're having trouble following things on IRC, the discussion page on the wiki might be a good place to leave comments and questions.<br />
<br />
In previous years we had talks in the day on a Friday, followed by pubbage in the evening and assorted activities on the Saturday. This seemed to work, so we'll follow a similar model this year.<br />
<br />
=== Timetable ===<br />
<br />
This is somewhat preliminary and subject to change as talks are confirmed or otherwise, but the overall structure should hold: <br />
<br />
{| class="wikitable"<br />
|-<br />
! Day !! Time !! Event<br />
|-<br />
| Friday or Saturday || 10am || People start arriving<br />
|-<br />
| || 10:30 am || Tea, coffee and biscuits<br />
|-<br />
| || 11am || Talks<br />
|-<br />
| || 1pm || Lunch<br />
|-<br />
| || 2pm || More talks<br />
|-<br />
| || 3pm || Tea, coffee and biscuits<br />
|-<br />
| || 3-30pm || Remaining talks<br />
|-<br />
| || 4:??pm || Functional Grit - small talks that may grow into functional pearls. Open session, anyone can give a quick talk!<br />
|-<br />
| || When people get hungry or the venue kicks us out || Food! Likely we'll head out for a curry<br />
|-<br />
| || Beer o'Clock || When everyone's finished eating, we'll head for a nearby pub<br />
|-<br />
| 2nd Day || To be confirmed<br />
|}<br />
<br />
=== Talks ===<br />
<br />
Volunteers please! Previously we have had a largely more practical set of talks than you might find at Fun in the Afternoon or an academic event. This was a good thing, and some of the best talks were from people who were far from considering themselves as experts, so feel free to tell us about your experiences.<br />
<br />
Talks planned and/or offered:<br />
<br />
* Claude Heiland-Allen - "mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets"<br />
* Alex McLean - "tidal - live coding patterns with Haskell"<br />
* Simon Marlow - "Scheduling lazy evaluation on multicore"<br />
* Will Sonnex - "Zeno - automated proofs of Haskell programs"<br />
* Add your name here - Add your title here<br />
<br />
==== Abstracts ====<br />
<br />
People giving talks should add these as they have them :-)<br />
<br />
* [http://hackage.haskell.org/package/mandulia-0.4 mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets]<br />
<br />
Mandulia provides a zooming visualisation of the Mandelbrot Set as many Julia Sets. Featuring a profiled and optimized renderer, and a Lua configuration and scripting interface. <br />
<br />
<br />
* Zeno - automated proofs of Haskell programs<br />
<br />
Zeno is an inductive theorem prover for properties of Haskell functions operating on recursive datatypes. Stuff like "drop n (take m xs) = take (m - n) (drop n xs)".<br />
<br />
<br />
* Title here<br />
<br />
abstract goes here<br />
<br />
==== Functional Grit ====<br />
<br />
In previous years there has been a successful 'functional grit' section. Usually an informal session for people to briefly talk/demo works in progress, no need to pre-register, just turn up and talk. Think small stones that might turn into functional pearls. If there's time it'd be great to do again this year.<br />
<br />
=== Other activity ===<br />
<br />
After Friday's talks, food and drink would be a good idea! Curry is traditional and probably the default, but we're open to other suggestions. After that, we'll retreat to a pub for the evening.<br />
<br />
<br />
[[User:DWright|Derek Wright]]<br />
<br />
[[Category:Events]]</div>Willhttps://wiki.haskell.org/index.php?title=AngloHaskell/2010&diff=36671AngloHaskell/20102010-09-06T14:16:04Z<p>Will: </p>
<hr />
<div>AngloHaskell 2010 is taking place on the 10th and 11th of September in Cambridge, UK (yes, tradition has been broken and month has changed!). It's free, and everyone is invited! Simply add your name to the wiki and we'll see you there.<br />
<br />
Organisational contact: Derek Wright<br />
<br />
== Dates and Venues ==<br />
<br />
{| class="wikitable"<br />
|-<br />
! Date !! Venue<br />
|-<br />
| Friday 10th September || Microsoft Research, Cambridge, UK<br />
|-<br />
| Saturday 11th September || A less formal venue (to be organised, any suggestions?)<br />
|}<br />
<br />
== Attendees ==<br />
<br />
Per last year, all attendees should '''bring or make a nametag''' that identifies you by your real name and/or IRC name. If anyone wants to drag a roll of stickers and a pen along that'll help!<br />
<br />
If you can't make the start on Friday, or can only make it on Saturday, that's fine. If you're not sure where everyone's going to be, give one of the contacts a call or a text.<br />
<br />
=== Definite ===<br />
<br />
* Derek Wright (Fri + Sat)<br />
* Graeme Burnett (Fri + Sat)<br />
* Neil Mitchell (hopefully Fri, definite Sat)<br />
* Sam Martin (Fri but not Sat)<br />
* Eric Kow (Fri + Sat)<br />
* Richard Smith (Fri only)<br />
* Benedict Eastaugh (Fri only)<br />
* Simon Marlow (Fri only)<br />
* Tristan Allwood (Fri only)<br />
* Magnus Therning (Fri)<br />
* Tony Cowderoy (Fri + Sat)<br />
* Philippa Cowderoy (Fri + Sat)<br />
* Will Sonnex (Fri)<br />
* Add your name here<br />
<br />
=== Possible ===<br />
<br />
* Claude Heiland-Allen<br />
* Joshua Lee Tucker<br />
* Ben May<br />
* Alex McLean (hopefully Fri, can't do Sat)<br />
* Richard Fergie (just Friday)<br />
* Max Bolingbroke<br />
* Roland Swingler<br />
* Vincent Hanquez<br />
* Rob Henderson (just Friday)<br />
* Louis Zhuang (hopefully Sat)<br />
* Add your name here<br />
<br />
=== Not this year, but hopefully next! ===<br />
<br />
* Add your name here if you can't make it this year<br />
<br />
=== Wifi Signup ===<br />
<br />
Wifi accounts are available on request. The signup deadline is Wednesday 8th September. Everyone wanting an account should provide:<br />
<br />
* Full name<br />
* Institution<br />
* Country of Residence<br />
* Email Address<br />
<br />
Signups here: <br />
<br />
If you'd prefer not to give details here, please email derek at obvious dot co dot uk with the subject "AngloHaskell Wifi Signup".<br />
<br />
* Derek Wright, Obvious Limited, UK, derek at obvious dot co dot uk<br />
* Philippa Cowderoy, , UK, flippa at flippac dot org<br />
* Add Full Name, Institution, Country of Residence, Email Address<br />
<br />
== Lodging ==<br />
<br />
It's likely that there'll be people in need of crashspace and so forth, so please organise here! Both offers and requests are good.<br />
<br />
=== Hostels ===<br />
<br />
Details coming soon...<br />
<br />
== Programme ==<br />
<br />
Planning will be taking place on IRC as per previous years: #anglohaskell on irc.freenode.net<br />
<br />
If you're having trouble following things on IRC, the discussion page on the wiki might be a good place to leave comments and questions.<br />
<br />
In previous years we had talks in the day on a Friday, followed by pubbage in the evening and assorted activities on the Saturday. This seemed to work, so we'll follow a similar model this year.<br />
<br />
=== Timetable ===<br />
<br />
This is somewhat preliminary and subject to change as talks are confirmed or otherwise, but the overall structure should hold: <br />
<br />
{| class="wikitable"<br />
|-<br />
! Day !! Time !! Event<br />
|-<br />
| Friday or Saturday || 10am || People start arriving<br />
|-<br />
| || 10:30 am || Tea, coffee and biscuits<br />
|-<br />
| || 11am || Talks<br />
|-<br />
| || 1pm || Lunch<br />
|-<br />
| || 2pm || More talks<br />
|-<br />
| || 3pm || Tea, coffee and biscuits<br />
|-<br />
| || 3-30pm || Remaining talks<br />
|-<br />
| || 4:??pm || Functional Grit - small talks that may grow into functional pearls. Open session, anyone can give a quick talk!<br />
|-<br />
| || When people get hungry or the venue kicks us out || Food! Likely we'll head out for a curry<br />
|-<br />
| || Beer o'Clock || When everyone's finished eating, we'll head for a nearby pub<br />
|-<br />
| 2nd Day || To be confirmed<br />
|}<br />
<br />
=== Talks ===<br />
<br />
Volunteers please! Previously we have had a largely more practical set of talks than you might find at Fun in the Afternoon or an academic event. This was a good thing, and some of the best talks were from people who were far from considering themselves as experts, so feel free to tell us about your experiences.<br />
<br />
Talks planned and/or offered:<br />
<br />
* Claude Heiland-Allen - "mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets"<br />
* Alex McLean - "tidal - live coding patterns with Haskell"<br />
* Simon Marlow - "Scheduling lazy evaluation on multicore"<br />
* Will Sonnex - "Zeno - automated proofs of Haskell programs"<br />
* Add your name here - Add your title here<br />
<br />
==== Abstracts ====<br />
<br />
People giving talks should add these as they have them :-)<br />
<br />
* [http://hackage.haskell.org/package/mandulia-0.4 mandulia: A zooming visualisation of the Mandelbrot Set as many Julia Sets]<br />
<br />
Mandulia provides a zooming visualisation of the Mandelbrot Set as many Julia Sets. Featuring a profiled and optimized renderer, and a Lua configuration and scripting interface. <br />
<br />
<br />
* Zeno - automated proofs of Haskell programs<br />
<br />
Zeno is an inductive theorem prover for properties of Haskell functions operating on recursive datatypes. Stuff like "drop n (take m xs) = take (m - n) (drop n xs)".<br />
<br />
<br />
* Title here<br />
<br />
abstract goes here<br />
<br />
==== Functional Grit ====<br />
<br />
In previous years there has been a successful 'functional grit' section. Usually an informal session for people to briefly talk/demo works in progress, no need to pre-register, just turn up and talk. Think small stones that might turn into functional pearls. If there's time it'd be great to do again this year.<br />
<br />
=== Other activity ===<br />
<br />
After Friday's talks, food and drink would be a good idea! Curry is traditional and probably the default, but we're open to other suggestions. After that, we'll retreat to a pub for the evening.<br />
<br />
<br />
[[User:DWright|Derek Wright]]<br />
<br />
[[Category:Events]]</div>Will