Jedna možnost specifikace chování programů jsou logické formule, které popisují relaci mezi vstupem a příslušným výstupem programu. Další krok je pak implementace dané specifikace konkrétním programem. Ideálně bychom ale chtěli vidět specifikované chování přímo ze specifikace ještě předtím, než existuje implementace. To znamená, že bychom chtěli i bez implementace mít možnost, pro danou specifikaci a daný vstup vypočítat příslušný výstup.
Obecně to není možné. Je to ale možné pokud se omezujeme na specifikace, kde všechny proměnné mají konečný rozsah. Takový přístup má např. jazyk RISCAL.
Cílem tohoto tématu je napsat řešič, který pro danou specifikaci v tomto jazyku a daný vstup vypočítá příslušný výstup. Uživatel pak má možnost provést specifikace podobným způsobem jako obyčejné programy, samozřejmě ale mnohem pomaleji.