Thursday, July 30, 2009

Static Analysis of Imperative Languages

Last year, I got the assignment to work through The Calculus of Computation by Bradley & Manna. The result is — in my humble opinion — a neat introduction to static reasoning for imperative languages. If you are new to that, but know a bit about predicate logic, then it might be a short and hopefully nice read to you.

Heuristics Methods for Inductive Invariant Generation in Pi explains the basics such as weakest precondition and strongest postcondition, why it is important to have inductive assertions for loops, why they are hard to find (hard as in undecidably-hard), and further what heuristics we could apply to simple standard cases to generate inductive assertions automatically.

If you enjoy it (or hate it), leave me a comment. Now, I finally found the option to notify me, when new comments come in, so that I have a chance to reply.

Wednesday, March 25, 2009

Patching for broken SD card readers

I had the pleasure to buy a broken SD card reader. It reports 2GB cards as 1GB cards. Here is a fix that allows you to force capacities onto the scsi disk kernel subsystem of the Linux kernel: scsi-capacity-setter.patch. The respective user space program is here capacity.c. You might want to use it in conjunction with some udev rules.

Friday, January 9, 2009

Liskell standalone

Some time has passed since I last blogged about Liskell. It is not dead nor have I changed my mind that Haskell needs a proper meta-programming facility not to mention a better syntax.

Liskell was a branch of GHC once. Now it sits on top of the GHC API, or I should rather say sneaks behind its back as it creates its own API as the original one is not suitable for the stunts I'm interested in. If Liskell sticks with GHC as its soil, I will definitely send patches upstream to refine the GHC API in the areas where it needs more flexibility for Liskell. However for the moment, my main target was to get something out that compiles with a stable version of GHC.

You can grab it with the usual
darcs get

This version has been tested with ghc 6.10.1 and should install like
./Setup.lhs configure
./Setup.lhs build
./Setup.lhs install
cd LskPrelude
make install-inplace
Optionally you can run make tests in the testsuite subdirectory. Thanks to for darcs hosting!