A szoftverfejlesztés nem matematika

A minap hallottam a JUM-on az egyik előadótól:

“Add ide a specit, és akkor megcsináljuk!”

Más alkalommal ugyanennek a személynek a szájából ugyanebben a kontextusban elhangzott az is:

“Jó lenne, ha valaki jól megcsinálná a követelményspecifikációt! Nem lennének benne ellentmondások, hiányzó részek…”

Tehát, aki ezt mondta, az azt feltételezi, hogy egy követelményspecifikációt meg lehet úgy (formalizáltan) írni, hogy abból egyértelmű és teljes legyen a feladat.

Erről két ismerősöm beszélgetése jut eszembe. Az egyik egy programozó matematikus (fiú), a másik pedig egy ügyvéd (lány). A srác azt kívánta, bárcsak olyan világban élnénk, ahol a (jog)szabályok annyira egyértelműek lennének, hogy nem lenne szükség ügyvédekre, bírókra.

Ezt a problémakört a jogi egyetemeken jogelméleti órákon tanítják. A lényege a dolognak, hogy ha a világunk a srác által kitalált “minden élethelyzetre van egy szabály” típusú lenne, akkor a rendszer túlszabályozott lenne. Ennek eredményeképpen a szabályrendszer abszolút rugalmatlanná és irtózatosan bonyolulttá válna. A bonyolultság miatt az értelmezhetőség lehetősége is kérdésessé válik, ami még azt is eredményezi, hogy a rendszer ellentmondásossá is válik. (A jelenlegi magyar jogrend sok területéről a jogászoknak már ma is az a véleménye, hogy eleve túlszabályozott.)

Ha a másik oldalról közelítjük meg, és nincsenek a legapróbb részletekig, minden élethelyzetre megfogalmazva a szabályok, akkor azok követése sem lehet egyértelmű. Ezért van az, hogy a bíró (tehát egy ember) dönti el, hogy bizonyított-e a vád, és hogy a vádlott – a jogszabályokban megfogalmazott kereteken belül – milyen büntetést kap.

A követelményspecifikáció problémája megegyezik az említett jogelméleti kérdéssel. Hogyan szeretnéd a szoftvert fejleszteni? Szeretnéd, ha több száz vagy ezer oldalas lenne a specifikáció? Meg fogod érteni? Kitől kérdezel?

A szoftverfejlesztés nem matematika.

Boncoljuk még, mire “jó” még a formalizmus!

ELTE: Bevezetés a programozáshoz c. tantárgy

Az ELTE-n úgy próbálják a hallgatókhoz “közelebb hozni” a programozást, hogy formális módszerekkel megtanítják nekik, hogy az mit is jelent.

Az idézet Fóthi Ákos: Bevezetés a programozáshoz c. könyvéből származik (2. javított kiadás, 6. fejezet, 76. oldal. ELTE-s jegyzet.)

Kapásból négy kérdés merül fel bennem:

  • Ennek a post-nak az olvasói közül (és – mondjuk – vegyük hozzá a Bevezetés a programozáshoz c. tárgy tanárát is), ki tanult meg úgy programozni, hogy egy ilyen módszert követett?
  • Hogyan magyaráznád el a ciklust egy kezdő programozónak?
  • Ki érti ezt egyáltalán?
  • Mire lehet használni?

Az első háromra nem válaszolok (mert szerintem a válasz egyértelmű). Mi van a negyedik kérdéssel? Azt mondhatnánk, hogy annak van értelme, hogy formálisan közelítjük meg a programírást, mert akkor bebizonyíhatjuk, hogy a program helyesen működik. Erre a BME-n is van tantárgy.

Hangsúlyozom:

a szoftverfejlesztés nem matematika.

BME: Formális módszerek c. tantárgy

A tárgy célkitűzései:

“Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis.

A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve.

A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a legfontosabb matematikai leíró paradigmákat, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket.

Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.”

Egy kis értelmezés:

  • “A rendszer nem csak funkcionalitásában legyen helyes” = azt csináljuk meg, amire szüksége van a megrendelőnek;
  • “Az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen” = amit meg kell csinálni (vagyis: amiről mi azt gondoljuk, hogy meg kell csinálni), azt jól csináljuk meg.

Mivel nem tudjuk pontosan, mit kell megcsinálni (ld. a követelményspecifikáció esetét), akkor hogyan is ellenőrizzük le, hogy helyesen működik az elgondolásunk?

(Megjegyzem, a Formális módszerek c. tárgyban tanított módszerek csak olyan kis állapottereknél működnek, amivel csak kis komplexitású szoftverek rendelkeznek. Egy akár már kisebb játék vagy üzleti alkalmazás is meghaladja ezt a komplexitási szintet.)

Mi értelme akkor ennek az egésznek?

A szoftverfejlesztés nem matematika.

Rakjuk össze!

Tehát ahogy eddig látjuk a helyzetet:

  1. Nem lehet megírni a követelményspecifikációt úgy, hogy abból el lehessen készíteni a szoftvert. Emberek kellenek ahhoz, hogy az elvárások végül megvalósulhassanak.
  2. A program nem egy matematikai formalizmus. Hiába ismerem a ciklus definícióját, nincs értelme (és a gyakorlatban nem is lehet) matematikai formalizmussal felírni a szoftvereket. Az egyénileg implementált algoritmusok emberi gondolkodást követnek.
  3. Nem lehet úgy programot készíteni, hogy annak a helyességét ellenőrizhessük. A program teszteléséhez emberek kellenek. Emberek mondják meg, hogy az készült-e el, amit vártak, és emberek állapítják meg azt is, hogy helyes-e a képernyőn megjelenő eredmény.

Mi valójában a szoftverfejlesztés?

A szoftverfejlesztésben egy valós életbeli problémára adunk megoldást. A fejlesztés folyamatában emberek vesznek részt: emberek mondják el, mit szeretnének, emberek kódolnak, emberek tesztelnek, emberek mondják meg azt is, hogy azt kapták-e, amit vártak.

Miért gondoljuk még mindig azt, hogy egy követelményspecifikáció legyen teljesen részletes, hosszú hónapokat töltsünk a megírásával, és eredményül több száz vagy ezer oldalakat kapjunk, amit végül már senki nem bír követni és megérteni? Miért hibáztatjuk mindig a követelményspecifikáció készítőit? Miért hisszük, hogy ha ez alapján tervezünk és tesztelünk, az jó lesz? Miért?

Amire valójában szükségünk van, az az emberek egymás közötti jó kommunikációja, és egymás iránti bizalma.

A szoftverfejlesztés nem matematika.

Share
This entry was posted in Módszertan and tagged , , , , , . Bookmark the permalink. Follow any comments here with the RSS feed for this post. Post a comment or leave a trackback: Trackback URL.

Comments

  • szerintem profizmus az, ha kijelentő módban közlöd azt amire más még gondolni se nagyon mer. grats ;)

  • Marhefka István

    Mar 24th, 2010

    köszi:)

  • Remélem nem én mondtam ezt egy gyenge pillanatomban :) Egyetértek egyébként, nekem is voltak érdekes élményeim az ELTE progmaton. Nincs kifogásom az ellen, hogy ilyet is tanuljunk, de hogy erre építsünk mindent, az elég súlyos.

  • Marhefka István

    Mar 24th, 2010

    Nem Te voltál az :) Én BME-s voltam, de vannak ELTE-s ismerőseim, ezért tudtam a fóthis féle példát felhozni :) Szerencsére nálunk nem vették ennyire “komolyan” a programozást. Amúgy egyetértek, hogy lássunk hasonlókat, csak helyén kell kezelni a dolgokat.

  • Azért nem _teljesen_ haszontalan szerintem a Fóthis világ. Pl. ha más nem, jól fejleszti az absztrakt gondolkodás képességét :) (Persze az is, ha klasszikus algoritmusokat olvasgatunk még akkor is, ha nincs szükségünk rá. Lehet, annak több haszna van.). Én a Fóthi féle elméletet mindig lenyűgözve néztem, mert azért elég szép szellemi szellemi magasságokat ér el. És még szebb az egészben, hogy tényleg mennyire nincs köze a valósághoz. A szürrealizmus harc.

    Szóval szerintem is igazad van. És jó a megfogalmazás.

  • Igazad van! De azért szólaltassuk meg a másik oldalt is. Én azért nyugodt vagyok, hogy az autómban lévő ABS-t vezérlő áramkör programhelyesség bizonyításon esett át, ugyanígy mondjuk egy repülőgép robotpilótája. Megvan a helye, de persze nem olyan alkalmazásoknál, amit mi fejlesztünk, ahova inkább két pszichológus, egy politikus, és három gondolatolvasó kell, és nem technológiai szakember (architect, bah!).

  • no ez azert nem ilyen egyszeru…formalisan felirni barmit, azert okec, mert minden nyelven okec :). Es mert nem az egyszeru majszosszaju programozok talaltak ki…szoftver helyesseg…verifikacio, validacio…hogyan ellenorzod, hogy helyes-e a programod, mikor te magad irtad :). Vannak okosok, akik kitalaljak mi a tuti “performance” ugyileg pl. formalizaljak ezeket, egy altaluk tervezett program megeszi a tiedet es kikopkodi a hibaidat, nem csak a szintaxisbelieket…es persze nem mindent, mert ember azert tenyleg kell, nem a programok komplexitasa az erdekes, hanem a szint amin gondolkodunk, azert mert kicsi, meg nem biztos hogy eleg, hogy azt latja a felhasznalo amit akart (ideig oraig)…mindemellett en sem irok fel semmit formalisan…vagy varjunk csak, egyszer felirtam, de az veletlen volt

  • [...] This post was mentioned on Twitter by István Marhefka, Balazs Brinkus. Balazs Brinkus said: Egesz jo kis cikk: http://infokukac.com/2010/03/a-szoftverfejlesztes-nem-matematika/ [...]

  • Marhefka István

    Mar 25th, 2010

    Viczi: Miből gondolod, hogy az autód ilyen típusú helyességellenőrzésen ment át?

    Biztosan hallottál már autóvisszahívásokról… Például legutóbb a Toyotának voltak gondjai…

  • Marhefka István

    Mar 25th, 2010

    repa: Pont arról szól a cikk, hogy az egész, amit írtál, nem működik. Lehet szerencsétlenkedni olyan programokkal, amik megpróbálják a hibákat megtalálni egy másik programban. Ez egy eszköz lehet, ami _segít_ a hibák feltárásában, de az teljesen reménytelen, hogy e program segítségével találjuk meg a hibákat a tesztelés alatt álló programunkban. (Btw. hány ilyen eszközt használtál már?)

    Kíváncsi lennék, mi lenne, ha ennek a programnak önmagát adnám meg :)

  • Egyetértek.

    A programozás inkább mérnöki tevékenység, mint matematika, akárcsak az építészet vagy a gépészet. Néha ki kell számolni dolgokat, de alapvetően a mérnöki hasnak van a legnagyobb szerepe.

    Lehet formálisan a program helyességét bizonyítani, de azt nem lehet _bebizonyítani_, hogy a hardver nem fog elromlani.

    Sőt, azt sem lehet garantálni, hogy a bemenő adatok jók lesznek. Lehet rájuk futtatni logikai ellenőrzéseket, de a jelentésüket csak az ember tudja, aki beküldi őket. Vannak is erre ismert példák: Elveszett Mars-szonda, megbokrosodott robotpilóta.

    Viszont -akárcsak más mérnöki tudományoknál- egy terv sosem árt.

  • Marhefka István: Nem azt mondom, hogy a tema amit a cikk feszeget alapvetoen rossz, vagy helytelen felismereseken alapul. A kijelentes, miszerint “A programozas nem matematika” trivialis…de a formalis nyelvek es elmeletek fontossagat, csak a mi szintunkon lehet ketsegbe vonni. Metrikak keszitese igen is lehetseges es ertelmes tud lenni (meg ha a teljesseg igenye nelkül is keszülnek, mert ha nem is mindent de eleget meg tud egy program talalni ahhoz, hogy az alkalmazas ne menjen at egy minoseg ellenorzesen…azt, hogy “hogy e program segítségével találjuk meg a hibákat a tesztelés alatt álló programunkban” nem en mondtam… egy indulo projektnel nyilvan nincs ertelme, automatizalni a vizsgalatokat, mert mind a mellet, hogy ezekkel majdnem ugyan akkora munka van mint magaval a programmal, abszolut nem rugalmasak es hatalmas koltsege lenne az aktualizalasnak). Sokat foglalkoztam tesztelessel, automatizalassal, metrikak keszitesevel, e mellett vagy ennek ellenere a cikk nagy reszevel egyet ertek, foleg azzal, hogy kezdo programozokat nem szabadna “formalitassal” traktalni, de ezen targyak letezese ertelmenek ketsegbe vonasaval nem ertek egyet…az hogy az emberek tobbsege egesz eleteben nem kap olyan feladatot, hogy hasznalja a fent emlitett targyakat, szinten lehetseges…viszont az emberek többsege nem is kepes “absztrakt” gondolkodasra.
    Minden esetre tetszik a post es a tema :)

  • Marhefka István

    Mar 25th, 2010

    Személy szerint imádom a matematikát. Hozzásegít a rendszeres gondolkozáshoz, a racionalitáshoz, absztrakcióhoz. Ez kell.

    Én a cikkben nem arra gondoltam, hogy a matematikának nincs helye a szoftverekben, csak arra a csapdára szerettem volna felhívni a figyelmet, hogy annak ellenére, hogy sok matekot tanulunk az iskolában, a szoftverfejlesztés folyamatában nem igazán lehet hasznosítani ezeket az ismereteket a követelmények formális leírására és az ez alapján történő szoftverellenőrzésre.

    Sokan úgy gondolják, hogy lehet. Az élet viszont nem így működik. (Egy-két nagyon speciális esettől eltekintve, amire Viczi is utalt.)

    Az említett tárgyak tematikája és célkitűzései abba a hamis illúzióba ringatják a hallgatót, hogy a világ így működik (vagy így kellene működnie).

    Ez a fajta félreinformálás már középiskolában is megfigyelhető, ahol a középiskolai informatikai tanárok, akik általában matematika szakosak is (és nem dolgoztak az iparban), matematikai próblémák megoldásán keresztül tanítják a programozást. (Számold ki programmal a kör területét, oldd meg a másodfokú egyenletet stb.)

    A cikk célja nem titkoltan az, hogy provokálja az olvasót, és felhívja a figyelmet arra, hogy a matematika eszköztára (itt a formális módszerekre gondolok) a szoftverfejlesztés napi folyamataiban nem játszik, játszhat szerepet. A problémák megoldásában fontosabbak az emberi kapcsolatok és az együttműködés.

    Köszönöm mindenkinek a kommentet! :)

  • Eloszor is hozzatennem, hogy a modszerek nagyresze nem 5 eve, hanem 40 eve keszult, amikor meg papiron adtak at a programkodot az azt begepelo emberkeknek. El tudod kepzelni ma, hogy ugy megirj egy Fourier trafot gepkozeli nyelven, hogy egy nap, mire eredmeny lesz belole? Ugy gondolom akkor igen is fontos volt formalizalni, es helyesseget bizonyitani. Vannak jelenleg is problemak, amik eloszor a matematika nyelven fogalmaznak meg, keresnek ra megoldast, es csak utana emelik at azt szamitogepre. Igaz, sokat valtozott a vilag azota, es manapsag olyan kodtomegek keszulnek, hogy lehetetlen lenne ezeket matematikai eszkozokkel verifikalni, de egy operacios kernel utemezojenek megtervezesekor nem gondolom, hogy Pistike leult, es a fol enter modszerrel addig reszelte a kodot, amig az el nem indult… Egyebkent meg a formalizmus egyik szerepe az ELTE-n, hogy egy matematikai szemleletet adjon, nem pedig hogy legszebb almodbol felkeltve is visszavagd a ciklus levezetesi szabalyat.

  • Marhefka István

    May 2nd, 2010

    Nucc: Te is áldozata lettél a provokatív posztomnak! Javaslom, olvasd el a kommenteket is.

  • Egykori Fóthi-tanítványként annyit fűznék hozzá, hogy az igaz, hogy “a szoftverfejlesztés nem matematika”, ellenben jócskán használ matematikai eszközöket.

    A ciklus programfüggvénye így nagy hirtelen valóban riasztónak hat, azonban emlékeim szerint nagyjából ez a “leghúzósabb” is, ha nem számítjuk a párhuzamos programozás bizonyos elemeit. Ha tudod, miről is szól, akkor meg lehet érteni, meg lehet tanulni.

    Követelményspecifikáció is jó lenne, ha lenne, de legtöbbször elegendő az informális, a formális – jó esetben – már maga a kód és a hozzá tartozó tesztesetek összessége. Jó esetben :).

  • Marhefka István

    Jun 6th, 2010

    Azt hiszem, megfogalmaztál egy nagyon fontos dolgot: maga a kód az, ami specifikálja a működést.

    Ha jól emlékszem, Joel fogalmazta meg a kövspecírásról: Amikor kövspecet írsz, ne légy profi!

  • [...] Egy szoftver jelenlegi ismereteink szerint nem tud hibamentes lenni. Ennek legfőbb oka, hogy egy szoftver nem matematikai alapokon készül. [...]

  • Csak most találtam rá erre e post-ra, és valami hasonlót követtem el nem olyan régen:
    http://pasztor.freeblog.hu/archives/2010/07/09/Az_IT_nem_alkalmazott_matematika/

    A történetnek (a programozás miért nem matematika) rengeteg vetülete van. Láttam már matematikust programozni, és az messze van attól mint amit ma a 21. században informatikának nevezünk.
    Ez az új tudomány vagy új iparág (kinek melyik tetszik) már annyira elkanyarodott a matematikai gyökereitől, hogy egyre kevésbé érdemes közös pontokat keresni.

  • Marhefka István

    Jul 27th, 2010

    akocsis: Akkor megelőztelek :) Viszont ezzel a témával meg Te előztél meg: http://pasztor.freeblog.hu/archives/2010/07/05/Az_IT_nem_gyrtsor/ :)

  • 1. A követelményspecet meg lehet formalizáltan írni! Ez tény! Mi változás? A specifikáció is termék, aminek vannak minőségi követelményei. Ha mellé tesszük, hogy a specifikációt javítani olcsóbb, mint egy éles rendszeren verziót váltani akkor azt is látjuk miért fontos. De mit is legyen a specifikációban? Az, hogy az ügyfél milyen üzleti eredményt akar elérni! MÉRHETŐEN! A megoldást hagyd a programozóra. (Ha meredeknek tartod azt, amit írok, akkor olvasd végig szépen a következő írásokat és érteni fogod mire utalok! http://www.malotaux.nl/nrm/English/WrkSlds.htm)
    Szerintem a specifikációt ott rontják el, hogy A) nem vizsgálják meg végterméki szempontból – review B) megoldási javaslatokkal tüzdelik tele

    2. A formális programhelyességről volt egy élménye. Még kicsi egyetemista voltam és ott tartottak valami országos diákkonferenciát, vagy micsodát. Volt egy hallgató, aki arról tartott beszámolót, hogyan lehet eltávolítani a programból a felesleges részeket. Mivel az elmélkedése igen matematikus volt (magyarán nem azt mondta, hogy futtasd le, mért le és ahová nem futott a program azt töröld) feltettük neki a frankó kérdést: Hogyan kerülnek bele azok a programrészletek, amik egyébként nem is kellenek! A válasz: Pl a programhelyességet igazoló invariánsok (aki tudja miről beszélek az érti, aki meg nem, annak mind1). No comment!

  • Marhefka István

    Oct 5th, 2010

    1. Én nem tartok meredeknek semmit, csak először meg szeretném érteni, mire gondolsz :) A két anti-patternnel egyetértek (nem vizsgálják meg végterméki szempontból, ill. hogy megoldási javaslatokkal tüzdelik tele).

    Nem tudom viszont, mit gondolsz formalizáltságon és minőségen. Én úgy gondolom, hogy nem lehet és nem is érdemes formalizáltan egy specifikációt megírni. A feladat formalizált leírása helyett inkább lazábban kell fogalmazni úgy, hogy abból egyértelműen kiderüljenek az ügyfél _elvárásai_. (És itt szándékosan fogalmaztam elvárásokat nem pedig követelményeket.)

    “Az, hogy az ügyfél milyen üzleti eredményt akar elérni! MÉRHETŐEN! A megoldást hagyd a programozóra.”

    Jó gondolat lenne, csak a fejlesztő megrendelés alapján működik, és már eleve lehet, hogy ott van elhibázva a dolog, hogy a rendszert nem is kellett volna kifejleszteni, mert nem lehet vele teljesíteni az elvárt üzleti eredményeket. Erről nem nagyon tehet a fejlesztő.

    De egyébként azzal mindenképpen egyetértek, hogy a megoldást hagyd a programozóra (én inkább fejlesztőt írnék a programozó helyett).

    2. Azoknak készült ez az írás, akik (még mindig) így gondolkoznak…

  • 1. Igazad van. Teljesen egyet is értek. Pont ezt a témát feszegeti Tom Gilb a Principles of Software Engineering Management könyvében. Zseniális olvasmány. Csak ajánlani tudom bárkinek.

  • Egyed Dániel

    May 9th, 2012

    Én az ELTE Programtervező informatikus szakjára járok,2. éves vagyok,Szoftverfejlesztő szakirányon,előtte Főiskolán Web – programozást tanultam.Rengeteg programot tervezek,és terveztem is,mielőtt Egyetemre jelentkeztem.A matematika rendkvül fontos,és a bevezetés a programozáshoz című tárgy ismerete alapnak számít,én szerintem.Egy BME-t ne hasonlíts az ELTE-hez,ott is elvégeztem egy szakot,angolu,nagyon híg volt,mellette nem tanultak semmit.Egy komolyabb program helyességét BIZONYÍTOTTAN be kell látnod,tudnod kell,hogy a program hogyan működik,és hibatűrő legyen.Nem sok ember érti meg Fóthi módszerének mondanivalóját,de én merem állítani,hogy rengeteget segített.A ciklus definíciója pedig egyszerű.. Nem csak a formalizmust kell tudnod,hanem értened is kell. A tárgy feltétele,hogy tudod,mit jelent a progarmozás.

  • @Egyed Dániel: en egy kezdo programozo vagyok. Magyarazd el kerlek a ciklus fogalmat.

  • Progmatos

    Nov 2nd, 2012

    Ebből a posztból süt a kezdő hozzáállás.

    Először is a ne hasonlítsuk a követelményspecifikációkat a jogszabályokhoz. A jogszabályokat azért nem lehet tökéletesen szabatosan megfogalmazni, mert az élet nagyon bonyolult. Egy szoftver közel sem olyan bonyolult, mint az élet. Még a legbonyolultabb sem.

    Másodszor a követelményspecifikációkkal nem az szokott a gond lenni, hogy nem tökéletesek, hanem hogy kimondottan rosszak. Nem kell tökéletesen specifikálni a feladatot, csak mondjuk 90%-ban. Ha már valaki BA, és az a dolga, hogy specifikációt írjon, akkor könyörgök, legalább az olyan dolgokra gondoljon előre, amik nekem az első 5 percben úgyis eszembe jutnak, és napokig fog állni a munka, míg a választ várom.

    Az “emberi kommunikáció” meg a “bizalom” nem segít azon, hogy nem tudok valamit megcsinálni, ha nincs megmondva, hogy mi az a valami. Specifikálni mindenképpen kell. A kérdés az, hogy ez mekkora időpocsékolással történik. Lehet szóban bizodalmaskodni meg emberi kommunikálgatni huszonötször apróbb részletenként külön-külön, vagy lehet írni egy fasza specifikációt, amibe csak néhányszor kell belejavítani a projekt során, és akkor is csak keveset. Az más kérdés, hogy az utóbbihoz szakértelem kell, és ez az, ami hiányozni szokott.

    Harmadszor helyességbizonyítást nem azért tanulunk, hogy a gyakorlatban írt szoftvereink helyességét formálisan bebizonyítsuk (bár speciális esetben erre is szükség lehet), hanem hogy kialakuljon az a szemlélet, ami ahhoz kell, hogy formális bizonyítások nélkül is többnyire bugmentes kódot írjunk. Aki tudja, hogy mi az az invariáns, az gyorsabban és kevesebb buggal kódol le egy ciklust, mint aki ad-hoc módon áll hozzá.

    Egyébként az ELTÉn volt két másik tárgy is, aminek a keretein belül formális módszereket tanulunk: a progmód (programozási módszertan elmélete), és a pp (párhozamos programozás). A bevprogot és a pp-t elég rossznak éreztem, de a progmód mindkét féléve nagyon hasznos volt. A második félév a párhuzamos programok helyességéről szólt. Aki írt már konkurrens kódot, az pontosan tudja, hogy ott a formális módszerek ismerete és megértése elengedhetetlen, mert az intuíció nagyon könnyen cserben hagyja az embert.

  • Progmatos

    Nov 2nd, 2012

    “[A]nnak ellenére, hogy sok matekot tanulunk az iskolában, a szoftverfejlesztés folyamatában nem igazán lehet hasznosítani ezeket az ismereteket a követelmények formális leírására és az ez alapján történő szoftverellenőrzésre.”

    A matekot speciell nem is arra kell hasznosítani, hanem matematikai jellegű problémák megoldására. Igen, a közhiedelemmel ellentétben van ilyen. Az, hogy te nem dolgoztál matematikai projekten, nem jelenti azt, hogy olyan nincs. Tele van az ipar matekkal, kezdve a pénzügyi moldellek implementálásával a 3D grafikai motorokon át az adatbányászaton keresztül az arcfelismerő szoftverekig.

    “Ez a fajta félreinformálás már középiskolában is megfigyelhető, ahol a középiskolai informatikai tanárok, akik általában matematika szakosak is (és nem dolgoztak az iparban), matematikai próblémák megoldásán keresztül tanítják a programozást. (Számold ki programmal a kör területét, oldd meg a másodfokú egyenletet stb.)”

    Na nehogy már egy sima középiskolásnak ipari szoftverfejlesztést akarjunk tanítani (szakközepesnek még hagyján). Miért kellene a kör területének kiszámításánál bonyolultabb dolgokat tanítani középiskolában? Ez kb. olyan, mintha művészettörténetből a gótikus stílusjegyek felsimerése helyett statikai számításokat akarnál tanítani.

    “hogy a matematika eszköztára (itt a formális módszerekre gondolok) a szoftverfejlesztés napi folyamataiban nem játszik, játszhat szerepet.”

    De szerepet játszik, csak nem közvetlenül. Lásd az előző hsz-emet.

    “A problémák megoldásában fontosabbak az emberi kapcsolatok és az együttműködés.”

    Ez mantrának jó, csak konkrétumok nélkül nem lehet mit kezdeni vele. Pontosan mit tanítanál egy egyetemen “emberi kapcsolatok és együttműködés” órán?

  • Marhefka István

    Nov 2nd, 2012

    Kedves Progmatos!

    Nem tudom, honnan vetted, hogy én nem dolgoztam matematikai projekten.

    Ha megnézed, amit írtam, én a “szoftverfejlesztés folyamatáról”, azaz módszertanáról írtam a cikkben.

    Én nem akarok igazságot tenni, hogy középiskolában mit kellene tanítani. Ezen vitatkoznak állandóan a tanárok. Az én elképzelésem szerint érdekes, kreativitást igénylő, projektszerű feladatokat kellene a tanároknak adniuk a diákoknak.

    Nagyon egyszerű az egyetemi kérdés is: projektszerűen dolgozzanak a diákok. Álljanak össze csapatok, amik féléves (vagy még rövidebb idejű) házi feladatokat fognak közösen megoldani. Ennyi.

  • Marhefka István

    Nov 2nd, 2012

    Progmatos (most reagálok az első kommentedre):

    “Ebből a posztból süt a kezdő hozzáállás.”

    Kérlek, írd meg a nevedet, és a blogodat, ahol megismerhetném, hogy Te hogyan állsz a szoftverfejlesztéshez, ahol neveddel vállalod a saját véleményedet a szakmában.

    “Egy szoftver közel sem olyan bonyolult, mint az élet. Még a legbonyolultabb sem.”

    Ezt én nem is írtam.

    “Másodszor a követelményspecifikációkkal nem az szokott a gond lenni, hogy nem tökéletesek, hanem hogy kimondottan rosszak.”

    Én nem is azt írtam, hogy tökéletesek legyenek, sőt, én kifejezetten gyűlölöm őket. A cikk arról szól, hogy vannak még olyan emberek, akik azt várják, hogy tökéletesek legyenek.

    “Az “emberi kommunikáció” meg a “bizalom” nem segít azon, hogy nem tudok valamit megcsinálni”

    Valszeg a kontextus nem jött át a szövegen. Én azokra a nagyvállalati (vagy inkább állami) projektekre gondoltam, ahol nem általlanak több ezer oldalas specifikációt is írni azért, hogy az alapján számonkérhető legyen a kivitelező.

    “Harmadszor helyességbizonyítást nem azért tanulunk, hogy a gyakorlatban írt szoftvereink helyességét formálisan bebizonyítsuk (bár speciális esetben erre is szükség lehet), hanem hogy kialakuljon az a szemlélet, ami ahhoz kell, hogy formális bizonyítások nélkül is többnyire bugmentes kódot írjunk. Aki tudja, hogy mi az az invariáns, az gyorsabban és kevesebb buggal kódol le egy ciklust, mint aki ad-hoc módon áll hozzá.”

    Maradjunk annyiban, hogy ez szerinted van így, meg azok szerint, akik az egyetemi tanrendet kialakították. Én inkább azt vallom, hogy már középiskolában vagy korábban kialakulnak (vagy nem) azok a skillek, ami alapján vki jó problémamegoldó lesz vagy sem.

    “Aki írt már konkurrens kódot, az pontosan tudja, hogy ott a formális módszerek ismerete és megértése elengedhetetlen, mert az intuíció nagyon könnyen cserben hagyja az embert.”

    Írtam és írok is ilyen kódot projektben. Nem segít, hogy elkezdek papíron bizonyítgatni.

  • Szerintem a cikk nem helyén kezeli a helyességbizonyítás témáját. A helyességbizonyítási elveket (amiket papíron is lehet, és fejben is lehet használni) algoritmusfejlesztéshez érdemes használni. Az ipari szoftverfejlesztés 99% interfészelés, és alig 1% algoritmusfejlesztés. A programozó idejének és energiájának javát a használt keretrendszer (nyelv, libek) szintaxisába ágyazott funkcióelérésre fordítja. Eközben minimális algoritmushasználat jellemző, itt-ott egy összegzés vagy keresés, maximumkiválasztás. A munka zöme a reprezentáció kialakítása, és interfészelése.

    A fenti elmélet akkor kezd hasznos lenni, amikor egy _részfeladat_ algoritmikus újdonságot tartalmaz. Hogyan gondoljuk végig, hogy az egy helyes megoldás-e? Hát zömmel a ciklus levezetési szabályai szerint gondolkodunk a ciklusokról. Akkor is, ha ezt papírra nem írjuk le. Ha valaki teljes mértékben elfordul ettől a témától, akkor számára a helyesség végiggondolása ekvivalens egy ad-hoc teszt set teljesítésével, és még arra sincs igénye, hogy a teszt set valamilyen axiomatikusan építkező logikai egységet fedjen le.

    Ha valaki sosem foglalkozik izgalmas részfeladatokkal, például a szoftverfejlesztési feladatai SQL interfészelések valamilyen divatos webes eszközön, és a megrendelők szinte egy az egyben SQL leképezhető funkciókat várnak el, akkor az ő számára valóban semmi használhatót nem tartalmaz ez az elmélet, hiszen még ciklust sem kell feltétlen megfogalmazzon egy olyan szoftver létrehozásához, ami teljes mértékben megfelel az elvárásoknak.

    A specifikáció egyértelműsége is hasonló. Az izgalmas részfeladatokban gazdag fejlesztéseknél fontos, hogy legyen egy olyan absztrakciós szint, ami már nem a megrendelő közvetlen befolyása alatt van, hanem arra való, hogy a fejlesztők között minimális legyen a félreértésekből eredő inkonzisztencia. A specifikációt a megrendelőtől elvárni természetesen baromság, a megrendelő nem programozó, nem tud specifikációt csinálni. Ez az architect dolga, aki akár papíron, akár forráskóddal oldja ezt meg.

  • flugi: A cikk arra próbálja felhívni a figyelmet, hogy sokan gondolják helytelenül azt, hogy a specifikáció upfront, pontos leírása fogja megalapozni egy projekt sikerét. “Ha pontosan leírtuk a követelményeket, akkor utána formális módszerekkel transzformálhatunk kóddá, vagy ellenőrizhetjük az elkészült program helyességét.”

    Hogy az algoritmustervezés, -fejlesztés “felsőbbrendű” lenne, mint az “ipari” szoftverfejlesztés, nézőpont kérdése. Én úgy gondolom, hogy sok esetben az algoritmusfejlesztés nem kunszt: különálló, absztrakt probléma megoldásáról van szó, amit elszigetelve a nagyobb probléma egyéb részeitől lehet kezelni.

    Ezzel szemben egy szoftverben megjelenő komplexitás (üzleti, architekturális, kód) kezelése sokkal szélesebb látókört, tapasztalatot és soft skilleket igényel.

    Nekem mind az algoritmusfejlesztés, mind a valódi szoftverfejlesztés izgalmas tud lenni.

  • Szvsz. van ennek értelme egy bizonyos szinten. Én személy szerint nem értek hozzá, egyedül tudományos cikkekben láttam ilyet, de nem is tervezek algoritmusokat, úgyhogy el tudom képzelni, hogy ahhoz kell, és érdemes használni.

  • Nagyon tetszett a cikk, köszönöm!

    Progmatos véleményéhez a középiskolai programozásról annyit: mi ötödölőt készítettünk, és óriási élmény volt utána a saját programoddal játszani.

Leave a Comment