Ako som u\u017e nieko\u013ekokr\u00e1t spom\u00ednal, v\u00fdvoj softv\u00e9ru je transform\u00e1cia po\u017eiadaviek z\u00e1kazn\u00edka na funk\u010dn\u00fd softv\u00e9r. V z\u00e1sade by to nemusel by\u0165 probl\u00e9m, ak by to nebol proces viacf\u00e1zov\u00fd, dlhodob\u00fd a nez\u00fa\u010dast\u0148ovalo sa ho viacero r\u00f4znych profesi\u00ed alebo t\u00edmov. Ak by sa aj pominuli v\u0161etky tieto komplik\u00e1cie, tak tu ost\u00e1va e\u0161te samotn\u00e1 komplikovanos\u0165 cel\u00e9ho procesu, kde je potrebn\u00e9 sk\u013abi\u0165 r\u00f4zne po\u017eiadavky (funk\u010dnos\u0165, r\u00fdchlos\u0165, bezpe\u010dnos\u0165 at\u010f.). \u010cere\u0161ni\u010dkou na torte je, \u017ee ke\u010f sa kone\u010dne z oh\u0148a softv\u00e9rovej vyhne vynor\u00ed ukut\u00fd softv\u00e9r, m\u00f4\u017ee by\u0165 tak komplikovan\u00fd, \u017ee overi\u0165 ho vo\u010di p\u00f4vodn\u00fdm po\u017eiadavk\u00e1m nie je v\u00f4bec trivi\u00e1lne. Pr\u00e1ve na rie\u0161enie tak\u00fdchto probl\u00e9mov vznikli form\u00e1lne met\u00f3dy.<\/p>\n
Jedn\u00fdm zo sp\u00f4sobov, ako udr\u017ea\u0165 v\u00fdvoj softv\u00e9ru v smere, za ktor\u00fd si plat\u00ed z\u00e1kazn\u00edk, je pou\u017ei\u0165 agiln\u00e9 met\u00f3dy. Tesn\u00fd kontakt so z\u00e1kazn\u00edkom a \u010dast\u00e9 uvo\u013e\u0148ovanie softv\u00e9ru dok\u00e1\u017ee robi\u0165 divy a v\u00fdsledok m\u00f4\u017ee by\u0165 naozaj to, \u010do z\u00e1kazn\u00edk skuto\u010dne potrebuje (to nemus\u00ed by\u0165 to ist\u00e9, ako to, o \u010dom na za\u010diatku hovoril – ale to u\u017e je in\u00fd pr\u00edbeh). Aj ke\u010f som o\u010dit\u00fdm svedkom toho, \u017ee agiln\u00e9 met\u00f3dy dok\u00e1\u017eu celkom v pohode zvl\u00e1da\u0165 ve\u013ek\u00e9 dlhodob\u00e9 projekty a rad\u00edm sa medzi ich z\u00e1stancov, nie je to strieborn\u00e1 gu\u013eka, s ktorou zastrel\u00edte ka\u017ed\u00e9 mon\u0161trum. Napr\u00edklad tak\u00fdm cestuj\u00facim v Par\u00ed\u017eskom metre na linke 14<\/a> by sa v momente, ke\u010f ich vlak zastav\u00ed mimo stanice, asi len \u0165a\u017eko vysvet\u013eovalo, \u017ee oprava pr\u00edde v najbli\u017e\u0161ej aktualiz\u00e1cii. Cel\u00e1 t\u00e1 linka je toti\u017e riaden\u00e1 automaticky – bez \u0161of\u00e9ra. Toto riadenie je pekn\u00fdm pr\u00edpadom pre safe-critical syst\u00e9my. To s\u00fa tak\u00e9, kde chyba v produk\u010dnej prev\u00e1dzke m\u00f4\u017ee st\u00e1\u0165 niekoho \u017eivot. A pr\u00e1ve na tak\u00e9ho pr\u00edpady s\u00fa tu form\u00e1lne met\u00f3dy (pre dan\u00e9 metro je to konkr\u00e9tne B-met\u00f3da).<\/p>\n \u010co to teda form\u00e1lne met\u00f3dy s\u00fa? Je to mno\u017eina postupov a n\u00e1strojov na z\u00e1pis, transform\u00e1ciu a overenie po\u017eiadaviek na \u013eubovo\u013en\u00fd syst\u00e9m (ja budem \u010falej hovori\u0165 o syst\u00e9me softv\u00e9rovom). To znamen\u00e1, \u017ee pomocou nich dok\u00e1\u017eem po\u017eiadavky zap\u00edsa\u0165, n\u00e1sledne ich viem postupne transformova\u0165 na hotov\u00fd k\u00f3d a na z\u00e1ver e\u0161te v\u00fdsledn\u00fd syst\u00e9m sp\u00e4tne overi\u0165 vo\u010di po\u017eiadavk\u00e1m. A to pomocou striktn\u00fdch matematick\u00fdch n\u00e1strojov (nie n\u00e1hodou s\u00fa form\u00e1lne met\u00f3dy de\u0165mi informatiky, ktor\u00e1 m\u00e1 korene v matematike). Pr\u00e1ve v tom, \u017ee je to tak\u00fdto ucelen\u00fd syst\u00e9m a v tej striktnosti je najv\u00e4\u010d\u0161ia sila t\u00fdchto n\u00e1strojov. V\u010faka tomu toti\u017e bude dodan\u00fd softv\u00e9r, ktor\u00fd sp\u013a\u0148a po\u010diato\u010dn\u00e9 po\u017eiadavky. Str\u00e1ca sa v\u00e1gnos\u0165, ktor\u00e1 sa m\u00f4\u017ee objavi\u0165 pri \u00fastnom podan\u00ed alebo pri p\u00edsanom texte, pr\u00edpadne neform\u00e1lnych diagramov. V\u0161etko je navrhnut\u00e9 tak, aby do seba zapadalo.<\/p>\n Form\u00e1lnych met\u00f3d je stra\u0161ne ve\u013ek\u00e9 mno\u017estvo. D\u00e1 sa poveda\u0165, \u017ee denne vznikaj\u00fa nov\u00e9 prisp\u00f4soben\u00edm existuj\u00facich pre nejak\u00e9 konkr\u00e9tne po\u017eiadavky. Ve\u013ek\u00e9 mno\u017estvo z nich sa pravdepodobne nikdy neuplatn\u00ed v praxi (\u010do ale neznamen\u00e1, \u017ee nemaj\u00fa svoju hodnotu). Medzi najzn\u00e1mej\u0161ie patria Petriho siete<\/em>, Procesn\u00e1 algebra<\/em> alebo B-met\u00f3da<\/em>. Tak\u00fa form\u00e1lnu met\u00f3du si tak trochu viete predstavi\u0165 ako programovac\u00ed jazyk. Na jednej strane obsahuje nejak\u00fa syntax z\u00e1pisu alebo not\u00e1ciu kreslenia. Na druhej strane potom n\u00e1stroje pre pr\u00e1cu s t\u00fdmto z\u00e1pisom. Napr\u00edklad viete vytvori\u0165 model syst\u00e9mu a potom tomuto modelu posiela\u0165 vstupy a sledova\u0165, \u010do sa so syst\u00e9mom deje. Tak si viete otestova\u0165 funk\u010dnos\u0165 syst\u00e9mu pred jeho implement\u00e1ciou alebo porovna\u0165 existuj\u00faci syst\u00e9m s t\u00fdmto modelom. D\u00f4le\u017eit\u00e9 je, \u017ee z toho modelu viete ve\u013ea vlastnost\u00ed syst\u00e9mu odvodi\u0165 matematick\u00fdmi oper\u00e1ciami. A teda v\u00e1m form\u00e1lna met\u00f3da m\u00f4\u017ee da\u0165 odpove\u010f napr\u00edklad na ot\u00e1zku, \u010di sa syst\u00e9m dostane do nejak\u00e9ho konkr\u00e9tneho stavu (\u010di u\u017e \u017eiadan\u00e9ho alebo chybov\u00e9ho).<\/p>\n Ak m\u00e1te pocit, \u017ee st\u00e1le neviete presne, o \u010dom hovor\u00edm, ale pritom m\u00e1te stredn\u00fa alebo vysok\u00fa \u0161kolu technick\u00e9ho smeru, tak ve\u013emi pravdepodobne ste u\u017e s jednou form\u00e1lnou met\u00f3dou robili a asi ani o tom neviete. Ak ste mali nejak\u00fd predmet, ktor\u00fd s\u00favisel so slabopr\u00fadovou technikou pravdepodobne ste preberali aj Boolovu algebru. Aj ona je pova\u017eovan\u00e1 za form\u00e1lnu met\u00f3du. Konkr\u00e9tne na v\u00fdvoj \u010d\u00edslicov\u00fdch obvodov. Najprv sa zadefinuje spr\u00e1vanie v\u00fdstupov na z\u00e1klade vstupov a potom sa pomocou vzorcov robia transform\u00e1cie, a\u017e sa d\u00f4jde k zapojeniu konkr\u00e9tnych \u010d\u00edslicov\u00fdch obvodov. Podstatn\u00e9 na tom je pr\u00e1ve to, \u017ee ak ste pri tom odvodzovan\u00ed – transform\u00e1cii – dodr\u017eiavali pravidl\u00e1, tak v\u00fdsledn\u00fd syst\u00e9m bol v spr\u00e1van\u00ed de facto toto\u017en\u00fd s t\u00fdm, \u010do ste mali na za\u010diatku, len z\u00e1pis sa zmenil tak, \u017ee ste vedeli pod\u013ea neho vyrobi\u0165 cel\u00e9 zapojenie. A takto nejako form\u00e1lne met\u00f3dy funguj\u00fa. Len pre in\u00e9 pr\u00edpady syst\u00e9mov a in\u00e9 scen\u00e1re pou\u017eitia.<\/p>\n Ak je to v\u0161etko tak\u00e9 super, kde je probl\u00e9m? Pre\u010do sa nepou\u017e\u00edvaj\u00fa form\u00e1lne met\u00f3dy denne? Je to kv\u00f4li ich zlo\u017eitosti. Aby ste ich vedeli pou\u017e\u00edva\u0165, mus\u00edte ich dobre pozna\u0165 – mal by ich pozna\u0165 ka\u017ed\u00fd v t\u00edme. Ide\u00e1lne, ak s nimi vie pracova\u0165 z\u00e1kazn\u00edk. A to nie je m\u00e1lo. Taktie\u017e zni\u017euj\u00fa pru\u017enos\u0165. Mal\u00e1 zmena po\u017eiadaviek m\u00f4\u017ee znamena\u0165 prepo\u010d\u00edta\u0165 cel\u00fd syst\u00e9m. Ak sa vr\u00e1tim k pr\u00edkladu s Boolovou algebrou, tak zmena jedn\u00e9ho v\u00fdstupn\u00e9ho pinu na \u010d\u00edslicovom obvode sa ned\u00e1 zapracova\u0165 inak, ako znovuodvoden\u00edm cel\u00e9ho syst\u00e9mu. A to v\u0161etko znamen\u00e1, \u017ee form\u00e1lne met\u00f3dy s\u00fa drah\u00e9. Preto sa pou\u017e\u00edvaj\u00fa len tam, kde je to nutn\u00e9 (Boolov\u00e1 algebra je trochu v\u00fdnimka, preto\u017ee je pomerne jednoduch\u00e1).<\/p>","protected":false},"excerpt":{"rendered":" Ako som u\u017e nieko\u013ekokr\u00e1t spom\u00ednal, v\u00fdvoj softv\u00e9ru je transform\u00e1cia po\u017eiadaviek z\u00e1kazn\u00edka na funk\u010dn\u00fd softv\u00e9r. V z\u00e1sade by to nemusel by\u0165 probl\u00e9m, ak by to nebol proces viacf\u00e1zov\u00fd, dlhodob\u00fd a nez\u00fa\u010dast\u0148ovalo sa ho viacero r\u00f4znych profesi\u00ed alebo t\u00edmov. Ak by sa aj pominuli v\u0161etky tieto komplik\u00e1cie, tak tu ost\u00e1va e\u0161te samotn\u00e1 komplikovanos\u0165 cel\u00e9ho procesu, kde je […]<\/p>","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[5],"tags":[],"class_list":["post-25","post","type-post","status-publish","format-standard","hentry","category-informatika"],"_links":{"self":[{"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/posts\/25","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/comments?post=25"}],"version-history":[{"count":1,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/posts\/25\/revisions"}],"predecessor-version":[{"id":229,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/posts\/25\/revisions\/229"}],"wp:attachment":[{"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/media?parent=25"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/categories?post=25"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/spireng.sk\/en\/wp-json\/wp\/v2\/tags?post=25"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}