Miten koodia todistetaan bugittomaksi?

matemaatikkomies

Donald Knuth ei kai aina testannut koodiaan vaan todisti sen oikeaksi. Missä oppisi tällaista testaamista välttävää ja todistamiseen perustuvaa ohjelmointia? Olen koulutukseltani matemaatikko ja ajattelin, että voisiko minulla olla annettavaa IT-alalla todistamisen puolella. Vai onko koodin todistajia jo tarpeeksi? Ei kai, kun äskettäin oli juttua prosessorien bugeista.

17

4290

    Vastaukset

    Anonyymi (Kirjaudu / Rekisteröidy)
    5000
    • M-Kar

      Näin: https://fi.wikipedia.org/wiki/Matemaattinen_todistus

      Koodia ei useinkaan todisteta oikeaksi kustannussyistä. Prosessorit on niitä joissa sitä todistusta juurikin tehdään mutta onnistuivat sössimään kun siellä semmoiset liukuhihnat ja tilat, ja homma menee juuri siinä kohtaa hankalaksi jos on jotain tiloja jossain joita pitää huomioida.

    • simplestway

      Parasta varmasti todistaa debuggaamalla koodi bugittomaksi.

    • Mielivaltaisen koodin todistaminen oikeaksi on ratkeamaton, undecidable, ongelma matemaattisesti. Käytännössä esim suuria mikropiirejä on onnistuttu verifioimaan logiikalla. Mutta tuo tutkimus on liikesalaisuuden alla.

      • except-e

        Tuosta syystä en tule koskaan hyppäämään kuskittoman itseajavan kulkuneuvon kyytiin.

        Ihminen ei osaa tehdä täydellistä poikkeuksenkäsittelijää.


      • M-Kar

        "Mielivaltaisen koodin todistaminen oikeaksi on ratkeamaton, undecidable, ongelma matemaattisesti."

        Ei ole.

        Koodi voidaan todistaa oikeaksi ja sellaiseksi, että tietyt virheet ovat mahdottomia mutta se mikä on se haastavuus on se, että mistä saadaan oikea määrittely.

        Aina tarvitaan sitä inputtia myös määrittelyksi, että niin kauan kun määrittely on oikein, saadaan toteutuskin oikein.

        "Käytännössä esim suuria mikropiirejä on onnistuttu verifioimaan logiikalla. Mutta tuo tutkimus on liikesalaisuuden alla."

        Kyllä logiikalla tehtävävä verifiointi on hyvin tunnettua.


      • M-Kar
        except-e kirjoitti:

        Tuosta syystä en tule koskaan hyppäämään kuskittoman itseajavan kulkuneuvon kyytiin.

        Ihminen ei osaa tehdä täydellistä poikkeuksenkäsittelijää.

        Kun koodia todistetaan oikeaksi, on aika tavallista, että ei jouduta käsittelemään poikkeuksia.


      • Turbo-Urpo
        M-Kar kirjoitti:

        Kun koodia todistetaan oikeaksi, on aika tavallista, että ei jouduta käsittelemään poikkeuksia.

        Että et joutuisi poikamieslihasta kättelemään, sido se jeesusteipillä reiteen, riittävän tiukasti, hypotermian varalta putsaa vanhat savet puntista pois.


      • kdnznzmzmz
        except-e kirjoitti:

        Tuosta syystä en tule koskaan hyppäämään kuskittoman itseajavan kulkuneuvon kyytiin.

        Ihminen ei osaa tehdä täydellistä poikkeuksenkäsittelijää.

        "Ihminen ei osaa tehdä täydellistä poikkeuksenkäsittelijää."

        mutta kuitenkin paremman ja nopeamman kuin mitä itse on..


      • M-Kar
        kdnznzmzmz kirjoitti:

        "Ihminen ei osaa tehdä täydellistä poikkeuksenkäsittelijää."

        mutta kuitenkin paremman ja nopeamman kuin mitä itse on..

        Voidaan myös todistaa että useimpia poikkeuksia ei ole mahdollista tulla joten niitä ei myöskään tarvitse käsitellä.


    • Uskoisin, että yli 90% kaikesta koodista on bugista - jollakin tavalla.
      Tämä on todellakin hämmentävää mielestäni mutta ymmärrän koodaajia - heidän on
      pakko tehdä tulosta nopeasti ja käytännöksi on vakiintunut erilaiset jälkeenpäin pätsäykset,
      eli kun koodi julkaistaan, sen arvellaankin olevan bugista ja sitten tulee pätsejä ja taas pätsejä.

      Sitä se on kun pitää saada nopeaa tulosta..

      • M-Kar

        "Uskoisin, että yli 90% kaikesta koodista on bugista - jollakin tavalla."

        Enemmän. Lähes 100%. Vain harvoin halutaan bugitonta koodia. Sen haluamisen päättää se kuka rahoittaa koodin tekemisen.

        "Tämä on todellakin hämmentävää mielestäni mutta ymmärrän koodaajia - heidän on
        pakko tehdä tulosta nopeasti ja käytännöksi on vakiintunut erilaiset jälkeenpäin pätsäykset,
        eli kun koodi julkaistaan, sen arvellaankin olevan bugista ja sitten tulee pätsejä ja taas pätsejä."

        Ei pätsäykset tarkoita välttämättä mitään bugia. Ennemminkin kyse on siitä, että ohjelmia ei käsitetä olevan mitenkään muuttumattomia vaan jatkuvassa muutoksessa.


      • 102030405060
        M-Kar kirjoitti:

        "Uskoisin, että yli 90% kaikesta koodista on bugista - jollakin tavalla."

        Enemmän. Lähes 100%. Vain harvoin halutaan bugitonta koodia. Sen haluamisen päättää se kuka rahoittaa koodin tekemisen.

        "Tämä on todellakin hämmentävää mielestäni mutta ymmärrän koodaajia - heidän on
        pakko tehdä tulosta nopeasti ja käytännöksi on vakiintunut erilaiset jälkeenpäin pätsäykset,
        eli kun koodi julkaistaan, sen arvellaankin olevan bugista ja sitten tulee pätsejä ja taas pätsejä."

        Ei pätsäykset tarkoita välttämättä mitään bugia. Ennemminkin kyse on siitä, että ohjelmia ei käsitetä olevan mitenkään muuttumattomia vaan jatkuvassa muutoksessa.

        Kyllähän sitä yleensä halutaan bugitonta koodia, mutta budjetti asettaa rajan sille, mille tasolle käytännössä päästään.

        Harvapa sitä haluaa varta vasten bugista koodia . . .


      • M-Kar
        102030405060 kirjoitti:

        Kyllähän sitä yleensä halutaan bugitonta koodia, mutta budjetti asettaa rajan sille, mille tasolle käytännössä päästään.

        Harvapa sitä haluaa varta vasten bugista koodia . . .

        No sehän se kun ei ole maksuhaluja.

        Jokainen saa kyllä vapaasti tehdä itse bugitonta koodia.


    • AamukahviaKohtaKeitän

      Prosessorien verifiointia tehdään usein SAT-ratkaisijoilla (SAT Solvers):

      www.satlive.org

    • tieteestäkiinnostunut

      Mitenkähän tieteessä? Kuulemma ainakin tilastolliseen päättelyyn saa vain käyttää jollain tapaa "standardoituja" ohjelmistoja. Aika moni tieteilijä on todella pedanttinen ja tarkka. Onko tieteen tekemisessä koodi virheetöntä?

      • M-Kar

        Ei siellä mitään standardointia ole sovelluksissa. Ohjelmointikieliä on standardointu ja niillä voi sitä tilastollista päättelyä ohjelmoida ja silloin sitä ihan itse voidaan huolehtia että koodissa ei ole bugeja.

        Ohjelmointikielten totetuksissa voi tietysti olla bugeja, onhan sitä kääntäjäbugejakin olemassa. Aika olennaista on pitää se oma koodi selkeänä niin noihin ei käytännössä törmää. Niillä kuitenkin ajetaan kaikennäköistä koodia valtavia määriä. Joitakin ohjelmointivälineitä on kyllä perusteellisesti varmistettu riittävän laadukkaiksi että niitä voidaan käyttää sairaalavehkeissä tai lentokoneissa. Niissä nimittäin on vaatimuksia koodin laadulle, tieteen tekemisessä ei ole.

        Itseasiassa tieteentekemisessä tilanne on usein päinvastoin mitä tulee koodin laatuun. Tieteentekijät yleensä vain kyhäisee jotain kasaan mikä tekee jotain uutta ja jännää ja lopputulos on kyllä helposti ihan kuraa. Sovellusohjelmoijat yleisesti ottaen tekevät paljon laadukkaampaa koodia ja varsinainen ohjelmistokehitys vähän vaativampaa.


    • 102030405060

      Näitä sanotaan formaaleiksi menetelmiksi.

    Ketjusta on poistettu 0 sääntöjenvastaista viestiä.

    Luetuimmat keskustelut

    1. Martina oli sarjassaan tänään 32.

      Mutta eikö pyöräily ja uinti ole vahvempia hänellä kuin juoksu? Aikaa on vielä harjoitella ennen Frankfurtin kisoja.
      Kotimaiset julkkisjuorut
      208
      1683
    2. Sofia miksi soitit torstaina Stefanil ja pyysit käymään kun muka olet ahdistunut.?

      Oliko asia suunniteltu, kun pyysi käymään ja varmasti tiesi et miten Stefan asiaan suhtautuu.Oliko myös Seiskan toimittaja pyydetty tarkoituksella pai
      Kotimaiset julkkisjuorut
      101
      1635
    3. Stepuli itkee facessa

      Haluaisin pyytää julkisesti karseaa käytöstäni anteeksi lähimmiltä, naapureilta ja etenkin Sofialta! Ei ole missään olosuhteissa hyväksyttävää käyttä
      Kotimaiset julkkisjuorut
      101
      1544
    4. Sofia oli ainoastaan rahan takia suhteessa Stefanin ja Nikon kanssa.

      Järkyttävää miten Sofia on käyttänyt hyväksi näitä molempia miehiä ja rahat loppu niin vain haukkumiset tullut kiitokseksi heille.
      Kotimaiset julkkisjuorut
      254
      1405
    5. Voi kun menisi nyt Stefan katsoo tyttären uutta ponia, viettäisi aikaa hänen kanssa.

      Aika parantaa kaiken ja meillä kaikilla on elämässä vastoinkäymisiä ja yli kyllä pääsee ainakin ajan kanssa.
      Kotimaiset julkkisjuorut
      134
      1365
    6. Minä menetän sinut kokonaan

      Siksi olen paniikissa, sekaisin ja surullinen. Taitaa olla jonkinasteinen stressitila päällä. Toivottavasti sinulla on kaikki hyvin.
      Ikävä
      48
      901
    7. Suomi teki typeryyttään Venäjästä nyt konkreettisesti vihollisen, jota se ei aiemmin ollut.

      Venäjä ei ole uhannut Suomen turvallisuutta, eikä Venäjän ja Ukrainan välinen konflikti ole signaloinut minkäänlaista uhkaa Suomelle. Se "uhka" luotii
      Maailman menoa
      448
      885
    8. Onpas Martina valinnut sopivan laulun

      Storyssa kun Isben poni tulee, " älä vie lapsuuttani pois." Äiti se lähtee mieluummin panopuuksi hotelliin, kuin viettäisi senkin ajan lastensa kanssa
      Kotimaiset julkkisjuorut
      115
      885
    9. Veikkauksia milloin Venäjä hyökkää Suomeen?

      Veikkaan että se tapahtuu nopeasti, ehkäpä jo kesäkuussa. Suomi 5,5 miljoonan harvaan asuttu maa. Venäjä ei tarvitse suurta joukkoa Suomeen, joten kai
      Maailman menoa
      293
      835
    10. Uskomatonta miten "kassatyttö Sannasta" tuli hetkessä kuoleman kauppias.

      Demarit on kautta historian olleet "takinkääntäjien"mestariluokkaa kokoomuksen hihassa kiinni. Sannan arviointikyky petti täysin Naton suhteen, Brysse
      Maailman menoa
      347
      818
    Aihe