- Haskell-Cafe - Haskell.org

ANN: afv-0.0.0
by Tom Hawkins 12 Jan '10

12 Jan '10

Hi, Here is the first release of Atom's Formal Verifier (AFV) [1], a tool intended to verify Atom -- or human -- generated C code. With the help of the Yices SMT solver [2], AFV uses bounded model checking and k-induction to verify assertions in iteratively called C functions, such as an embedded control loop. For each assertion in a design, AFV will return a pass, a fail, or an inconclusive result -- or it will die trying. In addition to Yices, AFV needs GCC for C preprocessing. This is a very early release. There are many things missing including counter example generation, finite precision modeling, and basic model reduction. And they is a chance -- say about 100% -- that there are bugs with the modeling transformations. In addition, the list of unsupported C syntax is embarrassingly long: - recursive functions - non-unique top level names (e.g. top level names hidden with static) - loops - switch statements - pointers - arrays - type casting - non void functions - functions with arguments - structs - enums - unions - typedefs Still, AFV works well for the handful of tests I have tried so far. AFV comes with a simple example. To run: $ afv example # This generates afv.h and example.c shown below... // Provides assert and assume functions. #include "afv.h" // Periodic function for verification. Implements a simple rolling counter. void example () { // The rolling counter. static int counter = 0; // Assertions. GreaterThanOrEqualTo0: assert(counter >= 0); // The 'counter' must always be greater than or equal to 0. LessThan10: assert(counter < 10); // The 'counter' must always be less than 10. // Implementation 1. if (counter == 10) counter = 0; else counter++; // Implementation 2. // if (counter == 9) // counter = 0; // else // counter = counter + 1; // Implementation 3. // if (counter >= 9) // counter = 0; // else // counter++; // Implementation 4. // if (counter >= 9 || counter < 0) // counter = 0; // else // counter++; // Implementation 5. // counter = (counter + 1) % 10; } To run the verification on the example: $ afv verify example -k 20 example.c # Which returns... parsing example.c ... verifying assertion example.GreaterThanOrEqualTo0.assert ... inconclusive: unable to proved step up to max k = 20 verifying assertion example.LessThan10.assert ... FAILED: disproved basis in k = 11 These results state AFV was unable to prove the "GreaterThanOrEqualTo0" assertion and it disproved the "LessThan10" assertion. The different implementations in the example yield different results. Any feedback or questions are more than welcome. I would like to thank Benedikt Huber and friends for the language-c library [3], Ki Yung Ahn for the yices library [4], and the folks at SRI for their work on the Yices SMT solver. Without these tools and libraries, AFV would not have been possible. -Tom [1] http://hackage.haskell.org/package/afv [2] http://yices.csl.sri.com/ [3] http://hackage.haskell.org/package/language-c [4] http://hackage.haskell.org/package/yices

1 0

Windows Automation - COM package - HaskellDirect
by Günther Schmidt 12 Jan '10

12 Jan '10

Hi all, I want to use Sigbjorn's com-package to do some automation under Windows. There seems to be some program "HaskellDirect" wich can create Haskell modules from type-libs, it's mentioned in the examples to the com package on Sigbjorn's site http://haskell.forkio.com/com-examples . Cabal install com does not seem to build / install the program though. Does anybody know how to get it? Günther

1 0

short licensing question
by Sebastian Fischer 12 Jan '10

12 Jan '10

Hello Café, when writing a Haskell library that uses two other Haskell libraries -- one licensed under BSD3 and one under LGPL -- what are allowed possibilities for licensing the written package? PublicDomain? BSD3? LGPL? Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)

12 16

on Happstack - "embedded HTML"
by Günther Schmidt 12 Jan '10

12 Jan '10

Hi, I'm just introducing myself to Happstack. I come across an example page where HTML and haskell code is mixed. Is this how happstack produces html, it's haskell code embedded in HTML? Günther

3 2

Tokenizing and Parsec
by Günther Schmidt 12 Jan '10

12 Jan '10

Hi all, I've used Parsec to "tokenize" data from a text file. It was actually quite easy, everything is correctly identified. So now I have a list/stream of self defined "Tokens" and now I'm stuck. Because now I need to write my own parsec-token-parsers to parse this token stream in a context-sensitive way. Uhm, how do I that then? Günther a Token is something like: data Token = ZE String | OPS | OPSShort String | OPSLong String | Other String | ZECd String deriving Show

5 4

hackage build errors
by Keith Sheppard 12 Jan '10

12 Jan '10

Hello Cafe, I noticed on my package's hackage page there is a build failure message: http://hackage.haskell.org/package/txt-sushi I don't know if these are real errors or not (I don't experience them on OS X and it's pure Haskell code) but I did poke around and noticed that some popular packages on hackage also have build failures: http://hackage.haskell.org/package/xmonad http://hackage.haskell.org/package/haddock http://hackage.haskell.org/package/pandoc http://hackage.haskell.org/package/alex http://hackage.haskell.org/package/hlint ... so what should I make of these errors? Are they useful in some way or just a problem with the build environment? (If that's the case I think they should probably be removed since they're confusing for potential users) Best Keith -- keithsheppard.name

3 2

Haskell-iPhone mailing list?
by Tom Tobin 11 Jan '10

11 Jan '10

Is there a mailing list for efforts to get Haskell running on the iPhone? As I've been maintaining an iPhone app for my employer (and nearly foaming at the mouth with hatred for Objective-C), I'd love to see a more sane option in this space. I've seen the wiki page [1], but I'm not aware of any other space for collaboration here. [1] http://www.haskell.org/haskellwiki/IPhone

1 0

ANN: chp-2.0.0, chp-plus-1.0.0
by Neil Brown 11 Jan '10

11 Jan '10

Hi, I've just released version 2.0.0 of the Communicating Haskell Processes (CHP) message-passing concurrency library onto Hackage. The main change from 1.x is that I have split the functionality into two libraries: the core functionality remains in the chp package (now version 2.0.0), while some of the additional capabilities have been moved out to the new chp-plus package (version 1.0.0). This should help in the long run by keeping the packages from becoming too large, and by allowing me to trim the dependencies of the core chp package. I've written more about the changes here, for those who it will affect: http://chplib.wordpress.com/2010/01/11/splitting-chp/ This will require small changes to your build system if you're using CHP and you upgrade to the new versions. The new versions should also fix build troubles with GHC 6.12 -- let me know if you have any troubles installing under 6.10 or 6.12. Hackage links: http://hackage.haskell.org/package/chp-2.0.0 http://hackage.haskell.org/package/chp-plus-1.0.0 Thanks, Neil.

1 0

Update for type-level library (0.2.4)
by Seyed Hosein Attarzadeh Niaki 11 Jan '10

11 Jan '10

Dear Haskell developers, A new version of the type-level library for type-level programming is pushed into the development repository and uploaded to the Hackage database. This is only a minor update to fix the compatibility issues with base 4, GHC>=6.10 and cabal-install (not backward compatible). Bests, Hosein Attarzadeh

1 0

Cabal bug?
by Henk-Jan van Tuyl 11 Jan '10

11 Jan '10

L.S., I had a strange response from Cabal: >cabal upgrade hlint Resolving dependencies... cabal: cannot configure containers-0.3.0.0. It requires base >=4.2 && <6 For the dependency on base >=4.2 && <6 there are these packages: base-4.2.0.0. However none of them are available. base-4.2.0.0 was excluded because of the top level dependency base -any So, base-4.2.0.0 cannot be used, because any version of base is OK? Is this a bug in Cabal? Regards, Henk-Jan van Tuyl -- http://Van.Tuyl.eu/ http://members.chello.nl/hjgtuyl/tourdemonad.html --

3 2