Ponton’s site

Yay, another parser in Haskell! That was a Haskell week, but I’m glad I had an opportunity to recall this beautiful full-of-math language.

This program reads an annotated program — a program with assertions. Assertions are just logic formulas. We use them to describe the program state between instructions, ie. variable x is equal to variable y squared. But assertions cannot be random, they must be derived from Hoare’s logic axioms and rules (which base on the formal semantic of the language). How do we know if there is an derivation of a program?

Here verification condicitions come. They are logic formulas too, but generated from annotated program. If all of them are true, then the program is derivable. More information here: http://www.macs.hw.ac.uk/~air/hic-hisd/ and http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html. The whole point is about formal verification of programs. Nowadays compiler can tell only whether given program has a syntax or type error. It doesn’t know anything about how this program should work and can’t say something like: “This program certainly does not multiply matrices.”. Assertions are some way to tell the programmer’s intentions to the compiler: “This is my piece of code and it should multiply two matrices”, and thus, by generating verification conditions and using automated theorem proving it could say: “It does.”.

So after a boring digression… this program reads an annotated program in a simple imperative language and generates verification conditions. That’s all.

All files are here: http://srednikpe.org/src/vc/

Computer science and math, English computer science, haskell, math, my code

Just a few lines of code, written when I was slightly bored.

module Main where
 
data Token = Plus | Minus | Divide | Times | Num Integer
 
rpnEval :: [Token] -> Integer
rpnEval = rpnEval' [] where
		rpnEval' (i:s) [] = i
		rpnEval' s ((Num i):t) = rpnEval' (i:s) t
		rpnEval' (a:b:s) (op:t) = rpnEval' ((evalOp op a b):s) t
 
		evalOp Plus = (+)
		evalOp Minus = (-)
		evalOp Times = (*)
		evalOp Divide = div
 
toToken :: String -> Token
toToken "+" = Plus
toToken "-" = Minus
toToken "*" = Times
toToken "/" = Divide
toToken s = Num (read s)
 
main = do
	l <- getContents
	mapM print $ map (rpnEval . (map toToken) . words) (lines l)

Computer science and math, English haskell, my code

All right. I said I’ll show my jzwi source and here it is: http://www.srednikpe.org/src/jzwi/

It is almost ended. It doesn’t only check local variable if they have unique names. I’m too lazy to do that. But after all it works fine and quite fast (compared to other interpreters written by my colleagues).

To run jzwi program just run “jzwi program.jzw argument1 argument2 …”.

It’s all licensed on GPL (any version). There is no guarantee that it’ll work. ;)

Computer science and math, English, Open Source haskell, interpreter, jzwi, my code

Uff… I have nearly finished my jzwi interpreter, just few minor fixes I will make in a week…

JZWI means “Język z wykładu improved” (”Language from lecture improved”). On our programming language theory subject we defined syntax using BNF notation and then we define formal semantic of this language (which is quite simmilar to Pascal/ALGOL).

It was our lab project to write a parser, converter to xHTML/LaTeX, an interpreter or full compiler in Haskell. It wasn’t as difficult as I thought, but I had to rewrite many parts of the code, ’cause firstly I wrote only simply parser, then simply converter and then I decided to try interpreter.

It costed me few nights and days, but I am very happy, when I see how beautifully it runs insertion sort. ;) Full source will be uploaded within few days. I have to lay off from vim and ghc. ;)

Uff… maybe I’ll check insertion sort once more. :>

Computer science and math, English haskell, jzwi