Metody specifikace softwarových systémů mohou být neformální, bez přesně definované syntaxe a sémantiky, nebo naopak formální, kdy je syntaxe a sématika přesně daná. Je zřejmé, že náročnost zvládnutí metody stoupá s mírou formalizace dané metody. Bohužel, čistě formální metoda nutně musí vycházet z matematicky definovaných formulí a bývá pro běžnou praxi díky své náročnosti hůře použitelná. Kompromisem jsou metody semiformální, které sice nejsou postaveny na jazyce matematiky, ale využívají přesně daného specifikačního jazyka (obvykle grafického), který je kompromisem přijatelným pro širokou obec softwarových inženýrů. Předmět detailně seznamuje studenty s jazykem UML (Unified Modeling Language) definující v současné době standard v oblasti tvorby software a s jazykem OCL (Object Constraint Language) používaným k účelu formální specifikace a verifikace objektově orientovaných systémů. Součástí je i problematika představení různých typů návrhových vzorů a jejich použití při tvorbě softwaru.