Category Archives: Uncategorized

A formal grammar for Magic: the Gathering

For the sake of viewer convenience, the content is shown below in the alternative language. You may click the link to switch the active language.

I wrote an ANTLR4 formal grammar for Magic: the Gathering cards.

It turns this

A Magic: the Gathering card

Or, more specifically, it turns this

Reach
Undergrowth — When you cast this spell, reveal the top X cards of your library, where X is the number of creature cards in your graveyard. You may put a green permanent card with converted mana cost X or less from among them onto the battlefield. Put the rest on the bottom of your library in a random order.

Into this:

You can try it out here: https://soothsilver.github.io/mtg-grammar/ and you can download the grammar and the source code from https://github.com/Soothsilver/mtg-grammar.

Read more »

Magisterské státnice na Matfyzu

Tento článek popisuje, jak fungovala ústní magisterská státní zkouška z informatiky na Matematicko-fyzikální fakultě Univerzity Karlovy (MFF, Matfyz) v září 2017. (verze v Google dokumentu)

Přihlášení

Magisterská státnice se nazývá “ústní část státní závěrečné zkoušky”. Žádná písemná část neexistuje. Slovo “ústní” ji pouze rozlišuje od “obhajoby diplomky,” což je druhá část zkoušky. Není dělená na několik zkoušek podle předmětu (matematika/informatika) na rozdíl od bakalářské zkoušky. Na zkoušku je třeba se přihlásit před termínem uvedeným v harmonogramu, ale nelze se přihlásit dříve, než máte splněné všechny ostatní studijní povinnosti vyjma diplomové práce.

Read more »

Java Pathfinder Inspector

Přes léto 2016 jsem se účastnil programu Google Summer of Code, během nějž jsem aktualizoval a značně vylepšil aplikaci zvanou Java Pathfinder Inspector.

Java Pathfinder (JPF) is framework pro formální kontrolu programů napsaných v Javě. Jeho jádro sestává z virtuálního stroje pro bajtkód, který sám běží v Javě; to umožní, aby JPF instrumentoval kód a nahradil kritické instrukce svými vlastními variantami. JPF je velmi rozšiřitelný a existuje mnoh modulů pro různé druhy verifikace jako například modul pro symbolickou exekuci. JPF Inspector je jedním takovým modulem a soustředí se na možnost ladění.

JPF Inspector je nástroj pro pozorování a kontrolu běhu programu spuštěného na virtuálním stroji Java Pathfinder. Podporuje breakpoiny, krokování (dopředu i dozadu), a to na několika úrovních granularity, a umožňuje uživateli pozastavit program a prozkoumat jeho současný stav (vlákna, zásobníky, proměnné, objekty na haldě). Oproti standartním debuggerům jako GDB také umožňuje explicitní plánování vláken.

Toto je první softwarový projekt, za který jsem dostal skutečné peníze.

Je naprogramovaný v Javě.

Na tomto projektu jsem pracoval ve věku 23 let, v roce 2016.

Read more »