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

Ze względu na ciekawość:

serwisant komputerowy < nauczyciel informatyki < administrator < programista nudnych rzeczy (biznes, banki, przemysł, itp.) < programista ciekawych rzeczy < pracownik naukowy

Polskie, Przemyślenia marzenia, praca

Przez 4 miesiące pracowałem przy tworzeniu gry, w końcu mogę się czymś pochwalić. Na stronie www.tanadu.com można się już zapisać do wstępnych testów tytułowej gry. Póki co jeszcze nie można zagrać, ale można poczytać o samej grze oraz dowiedzieć się, że dla najlepszego testera jest przewidziana nagroda.

Tak to wygląda mniej więcej.

Polskie praca, tanadu

Mój nowy plan może wyglądać naprawdę groźnie, jednak buddyzm, IO (inżynieria oprogramowania) i PO (praktyka optymalizacji) powinny być w miarę łatwe, więc tak naprawdę zostaje tylko NLP (natural language processing) i SJP (semantyki języków programowania). Oba na szczęście nie wymagają jakiejś większej wiedzy (w szczególności JFiZO i AiSD). W tym semestrze potrzebuję dużo, dużo punktów… Kto mnie zmobilizuje?

Polskie, Real life masakra, plan zajęć, studia

Jedną z “dziwnych” rzeczy, które potrafią mi “zająć” czas, gdy się “nudzę”, jest “umieszczanie” losowych “słów” w cudzysłowy i “obserwowanie”, jak zdanie “zmienia” przez to swoje “znaczenie”.

Polskie, Przemyślenia dziwactwa, hehe

Nie mieliśmy kości na sesję, to trzeba było coś napisać. NWOD-owy rzucacz kośćmi w Pythonie:

#!/usr/bin/python
 
import time
import random
import sys
 
# argumenty: 
ile_scian = int(sys.argv[1])    # ilusciennymi koscmi rzucamy
sukces = int(sys.argv[2])       # od ilu oczek jest sukces
ile_rzutow = int(sys.argv[3])   # ile razy rzucamy
 
def kostka(sciany):
    rzut = random.randint(1, sciany)
    print rzut
    return rzut
 
print '------------------------------'
 
random.seed()
 
sukcesy = 0
 
for i in range(0, ile_rzutow):
    rzut = kostka(ile_scian)
 
    if rzut >= sukces:
        sukcesy += 1
 
    while rzut == ile_scian:
        print 'Przerzut!'
 
        rzut = kostka(ile_scian)
 
        if rzut >= sukces:
            sukcesy += 1
 
print
print "Sukcesy: ", sukcesy

Computer science and math, Polskie my code, python

Ten ascetyczny czarny mi się znudził, znalazłem (bo przecież nie stworzyłem) sobie fajny styl, ale trochę go trzeba będzie zmodyfikować: nowa chmurka tagów, która zastąpiła listę kategorii, nie ma marginesów, wszystkie linki stają się niebieskie, jak się na któryś najedzie myszką, oraz trochę dziwnie tytuł i menu wygląda na dole.

EDIT: Trochę mi się udało poprawić, tagi nadal średnio wyglądają i tytuł nie najlepiej.

Uncategorized meta

Debuggowanie potrafi niemal wykładniczo skrócić czas szukania błędów w programie, więc warto nauczyć się sprawnie obsługiwać debugger. Dotychczas GNU Debugger był dla mnie czarną magią, a wzorem — ten  z Visual Studio. Tylko gdzieś słyszałem/czytałem, że gdb ma takie same możliwości, ale nie dane mi było się o tym przekonać. Niedawno musiałem się nauczyć jego obsługi, dlatego napiszę sobie ściągawkę (nie, żeby z niej korzystać, ale żeby utrwalić).

Zanim zaczniesz

Musisz najpierw skompilować program z informacjami dla gdb. Robi opcja -g dla gcc.

Komendy

Zamiast miłego interfejsu graficznego, jest miły wiersz poleceń (co dla programisty jest wygodniejsze, bo nie musi odrywać rąk od klawiatury :>), w którym wpisujesz polecenia. Nie musisz podawać jej pełnej nazwy, wystarczy jednoznaczny początek (najczęstsze polecenia mają jedno/dwuliterowe synonimy). Działa dopełnienie tabulatorem! W razie czego: help komenda.

Start

Pierwszy paremtr to nazwa pliku wynikowego programu. Drugim może być numer procesu tego programu, jeśli chcesz zacząć debuggować już działający program.

Przydatne komendy:

• run [argumenty] -  uruchamia program z podanymi (opcjonalnymi) argumentami
• continue - jeśli program jest zatrzymany, wznawia jego działanie
• finish - program się wykonuje aż do napotkania “return”; innymi słowy program działa aż do końca aktualnej ramki stosu

Stop

Żeby się gdzieś zatrzymać, trzeba ustawić breakpointy:

• breakpoint funkcja - ustala breakpoint na początek funkcji
• breakpoint [plik:]linia - ustala breakpoint na określoną linię pliku
• info breakpoints - wypisuje utawione breakpointy
• delete n - usuwa n-ty breakpoint
• condition n cond - ustala warunek dla n-tego breakpointa (program zatrzyma się na nim, jeśli zostanie spełniony warunek cond)
• ^C - czyli przerwanie z klawiatury, również zatrzymuje działający program i oddaje kontrolę gdb

Co się dzieje?

Kilka przydatnych komend, aby zorientować się, co się aktualnie dzieje:

• list - listing kodu (10 linii obecnego kontekstu, podana nazwa funkcji, numer linii, etc.)
• frame - aktualna ramka stosu oraz aktualna instrukcja
• backtrace - ślad stosu
• print x - wypisanie wartości x (to może być dowolne wyrażenie, razem ze zmiennymi w programie)

Tropimy

To, co najważniejsze, czyli śledzimy program krok po kroku:

• next - następna instrukcja (lub n instrukcji), bez wchodzenia wgłąb procedur
• step - j/w, ale z wchodzeniem wgłąb

Psujemy

Można przetestować kilka rzeczy w trakcie trwania programu:

• set x wartość - ustawiamy zmiennej x wartość
• call f(x) - wywołujemy funkcję f z argumentami (w tym wypadku tylko x)

Format zapisu zmiennych, funkcji i adresów.

Czasem chcemy się odwołać do zmiennej z jakiegoś innego zakresu albo funkcji składowej, wtedy piszemy zakres::x, jeśli np. zakres jest klasą, a x jej metodą/polem, albo zakres jest funkcją, a x jej zmienną lokalną. Odwołanie do konkretnej linii ma składnię plik:linia, np. test.c:244. Adres zapisujemy z gwiazdką na początku, np. *0×000000.

A na koniec: quit. I tyle. To było zaledwie 1/5 możliwości gdb, mimo to spokojnie wystarczy do efektywnego debuggowania. Chociaż dziesiątki printfów mają swój urok. ;)

Computer science and math, Open Source, Polskie debug, gdb

Spróbowałem zrobić pizzę, prawie mi wyszło - z wyjątkiem niedopieczonego ciasta…

Więcej.

Polskie, Real life fail, jedzenie, pizza