FW: catch tests

[Dimitrios Vytiniotis]

FIY. 

Nathan and I will start looking at the examples and porting them. 

---

From: Neil Mitchell [ndmit...@gmail.com]
Sent: Tuesday, December 20, 2011 2:42 PM
To: Dimitrios Vytiniotis
Subject: Re: catch tests

Hi Dimitrios,

Very interesting! I would love to see what you come up with.

All my toy examples are in http://community.haskell.org/ndm/darcs/catch, which you can darcs get - see the examples directory. I also checked hscolour and finitemap, see my HW paper for details. Note that most of the nofib suite can be made to crash with ease, so they aren't that interesting for this problem.

Thanks, Neil

On Tuesday, December 20, 2011, Dimitrios Vytiniotis <dimi...@microsoft.com> wrote:
>
> Hey Neil, I hope you are well!
>
> I have  a quick question: Do you have some testsuite on catch somewhere?
> (I know you probably run the whole nofib testsuite but do you have some smaller 'interesting' subset
> of small-to-medium-size programs somewhere that we could download and use?)
>
> The context is that Simon and I and Koen and our intern Nathan Collins are developing a system for
> checking Haskell contracts using a first-order theorem prover and definitely want to be able to catch
> all or most catch programs (perhaps by annotating them, but still)
>
> Thanks!
> d-
>
>
>
>
>

[Dimitrios Vytiniotis]

BTW the correct URL is:

http://community.haskell.org/~ndm/darcs/catch

---

From: haskellc...@googlegroups.com [haskellc...@googlegroups.com] on behalf of Dimitrios Vytiniotis [dimi...@microsoft.com]
Sent: Tuesday, December 20, 2011 10:25 PM
To: haskellc...@googlegroups.com
Subject: FW: catch tests

[Nathan Collins]

I ported his first regression test, Ants.hs [1] [2]. The
regression tests are nice because they are shorter, and he has
annotated them with the "contract", which in this case is 'shortest
::: CF -> CF', where

shortest xs = foldr1 shorter (map path (permutations xs)) ;;

So, in particular, this example is genuinely higher order. Strangely
to me, it's counter satisfiable if I instead use

shortest = foldr1 shorter `o` map path `o` permutations ;;

for 'o' function composition. I use 'o' to define 'concatMap', which
is used indirectely by 'shortest'. Anyone see why the point-less
version would be different?

Out of 16 contracts I added, 14 are simple

Cf^n -> CF

annotations, which we think could be discovered automatically. The
two "non-trivial" contracts are

{-# CONTRACT
permutations ::: CF -> (CF&&{xs: not (null xs)})
#-};;

{-# CONTRACT
foldr1 ::: (CF -> CF -> CF) -> (CF&&{xs: not (null xs)}) -> CF
#-};;

I.e., 'permutations' is compatible with 'foldr1'.

Takes 69s to check all contracts, and 29s to check just 'shortest'.

Hopefully I actually implemented all these functions correctly ... the
patch is [2].

-nathan

[1] http://community.haskell.org/~ndm/darcs/catch/examples/Regress/Ant.hs
[2] https://github.com/cpa/haskellcontracts-examples/commit/a3178b9f9b455d162cb71a34ffa96384f2240096

[Nathan Collins]

On Wed, Dec 21, 2011 at 9:10 PM, Nathan Collins
<nathan....@gmail.com> wrote:
> I ported his first regression test, Ants.hs [1] [2].  The
> regression tests are nice because they are shorter, and he has
> annotated them with the "contract", which in this case is 'shortest
> ::: CF -> CF', where
>
>  shortest xs = foldr1 shorter (map path (permutations xs)) ;;
>
> So, in particular, this example is genuinely higher order.  Strangely
> to me, it's counter satisfiable if I instead use
>
>  shortest = foldr1 shorter `o` map path `o` permutations ;;
>
> for 'o' function composition.  I use 'o' to define 'concatMap', which
> is used indirectely by 'shortest'.  Anyone see why the point-less
> version would be different?

Looked at the 'o' version a little with Dimtrios. We didn't figure
out yet, but the .tptp file is attached. We added an unhelpful
contract for 'o'

{-# CONTRACT
o ::: (CF -> CF) -> (CF -> CF) -> CF -> CF
#-};;

[Simon Peyton-Jones]

| Takes 69s to check all 16 contracts, and 29s to check just 'shortest'.

Great. It's good news that they all go through!

Simon