Symbolinen analyysi

Symbolinen analyysi on metateoria, kuinka käyttää tulkintoja symbolien välisten suhteiden ymmärtämissä. Symbolista analyysia voidaan tehdä tietokoneella automaattisten työkalujen avulla tai sitä voi tehdä ihminen.

Symbolisen käsittelyn historiaa

Pohjan symboliselle käsittelylle loi 1930-luvulla Alonzo Church, jonka ansiosta syntyivät myös käsitteet laskettavuus ja lambda-kalkyyli sekä olennainen osa tietokoneen peruskonstruktiota . Lähdekoodin symbolinen käsittely tuli eri muodoissaan muotiin 1970-luvulla, jolloin tutkittiin symbolista suorittamista, symbolista evaluointia ja symbolista analyysia. Menetelmät olivat poissa muodista 20-30 vuotta, kunnes vuoden 2000 jälkeen uudestaan on pyritty tutkimaan ohjelmien suorittamista ajamatta niitä lopullisessa muodossaan. Churchin merkittävästä työstä huolimatta viime aikoihin asti on ollut epäselvää, mitä symbolinen käsittely ja analyysi itse asiassa ovat ja miten ne liittyvät ihmiseen tiedon tulkitsijana. Vasta vuonna 2008 pystyttiin ensimmäisen kerran linjaamaan ihmisen suorittama ja tarvitsema symbolinen tieto ja tietokoneen antama tuki. Alla kuvataan tämä periaate.

Kielten ymmärtäminen symbolien kautta

Kaikkien kielten perusyksikkönä on symboli. Kaikki formaalit esitykset, myös ohjelmistojen kuvaamisessa yleisesti käytetyt UML-kaaviot, koostuvat symboleista. Symbolit kuvaavat objekteja tai ilmiöitä. Objektien ymmärtäminen tapahtuu alimmalla tasolla tekemällä symbolien ja objektien välisiä tulkintoja. Symboli on Charles Peircen käsitteistössä erikoistapaus termistä merkki.

Analyysin määritelmän mukaan symbolinen analyysi on prosessi, jolla monimutkaisia rakenteita voidaan ymmärtämisen helpottamiseksi pilkkoa pienempiin osiin. Pilkkomisen lisäksi yleensä on tarkasteltavista symboleista tarpeen luoda horisontaalisia selityksiä (selitys) ja hierarkkisia käsitteitä (käsite). Peircen mukaan selitys saadaan aikaan päättelyllä. Näin tapahtuva (argumentointi) voi olla logiikasta riippuen deduktiivista (Deduktiivinen päättely), induktiivista (Induktiivinen päättely) tai abduktiivista (Abduktiivinen päättely).

Symbolisen analyysin periaate

Kehys symboliselle analyysille on seuraava

Nr	Metakäsite	Määrittely
1	Symboli	Ymmärtämisen peruskäsite
2	Objekti	Mitä on symbolin takana
3	Tulkinnos	Johtopäätös symbolien ja objektien kytkemiseksi keskenään.
4	Logiikka Symbolinen logiikka (engl. Symbolic logic)	Periaate, jolla tulkinnan yhdistetään toisiinsa. Eri objekteilla on oma logiikkansa.
5	Kysely (engl. Query)	Formuloitu kysymys, joka aloittaa päättelyn kyseessä olevassa logiikassa
6	Tulos (vastaus kyselyyn)	Logiikan antama tulos symbolisen informaation muodossa
7	Pragmatiikka eli merkitys	Saadun informaation (tuloksen) tärkeys tarkoituksena kattaa aiottu tavoite.

Esimerkki: Symbolinen analyysi liikenteessä

Kuvataan tilannetta, jossa henkilö NN on palaamassa autolla kotiin tai menossa harrastuksiin tai töihin:

1. Tärkeä havainnoitava symboli tiellä on liikennevalo, jokaisessa isommassa risteyksessä.
2. . Liikennevalo (symboli) kuvaa sen takana olevaa objektia, eli risteystä.
3. Symboliin kohdistuva tulkinta on näköhavainto, joka kertoo liikennevalon värin. Jos valo on vihreä, NN voi jatkaa matkaansa. Muuten hänen täytyy odottaa. Tietokoneessa tulkintoja vastaa tietokoneen alkeistoiminto, komputaatio, joka alimmalla tasollaan vastaa konekielistä lausetta ja lähdekooditasolla yhtä ohjelmakoodin lausetta, jonka kääntäjä pilkkoo konekielisiksi lauseiksi (konekielinen käsky).
4. Tulkinta kuuluu laajempaa kokonaisuuteen eli logiikkaan (liikennesäännöt), joka tarvitaan, jotta voitaisiin käyttäytyä liikenteessä vaarantamatta muita. Logiikka voidaan yleensä määritellä sääntöinä, mutta vielä sujuvammin ns. tilasiirtymäkaavioina (tilakaavio).
5. Kysely on formuloitu kysymys, joka käynnistää tilanteen mukaan logiikan, kuten liikennesäännön.
6. Tulos on paluu logiikasta, siis vastaus kyselyyn.
7. Pragmaattinen merkitys tarkoittaa jotakin hyötyä NN:lle. Hän saa hyötyä siitä, että pystyy jatkamaan matkaansa – vaarantamatta itseään risteyksessä. Jotta NN pääsisi määränpäähänsä, hän joutuu tulkitsemaan symboleita perättäisiä ja sisäkkäisiä kyselyitä käyttäen. Navigoinnin logiikka on esimerkki korkeamman tason logiikasta, joka aktivoi oman reittinsä, jolla tarvitaan omat liikennevalonsa ja alemman asteen logiikan toiminnot.

Symbolisen analyysin rajoitukset

Kaikki asiat eivät ole yhtä yksinkertaisia mallinnettavia kuin äskeinen. Toisaalta aina ei löydy yhtä selkeitä indikaattoreita kuin liikennevalo. Erilaisia ääripäitä kuvaavat kaksi filosofian suuntausta:

1. Analyyttinen filosofia ja erityisesti looginen atomismi lähtee siitä, että käsitteet voidaan jakaa rajattoman pitkälle osiin. Atomismin mukaan kaikki aine koostuu jakamattomista osista.

1. Toisaalta mannermainen filosofia joka tarkastelee monimutkaisimpia ilmiöitä, joista osa on jopa mahdoton ymmärtää. Siihen liittyvä käsite holismi kritisoi läntisen tieteen perinteistä näkemystä, jonka mukaan tutkimusongelma yleensä ensin jaetaan osiin ja ongelmaa selvitetään sitten osa kerrallaan.

Vaikeuksia hahmottaa mihin kukin symboli todellakin viittaa, kutsutaan yhteisellä nimellä symbolin maadoittamisen ongelmaksi. Jos samalle symbolille tai symbolien joukolle on monta vaihtoehtoista tulkintaa, puhutaan monimerkityksellisistä (ambiguous) tilanteista (context). Silloin kun täsmällinen objekti aina voidaan tunnistaa, voidaan symbolien välille määritellä formaaleja vuorovaikutuksia, esimerkiksi predikaattilogiikan keinoin. Ohjelmistoatomi on käsite, jonka avulla täsmällisiä objekteja voidaan luoda kytkemään muita objekteja yhteen

Seuraavassa autoilijan logiikka liikennevaloissa:

Tilan nr	Tila	Ehto	Seuraava tila	Tulkinta (havainnot)
1	Aloitus	-	Odotus
2a	Odotus	Keltainen	Odotus	Havaitaan keltainen valo
2b	Odotus	Punainen	Odotus	Havaitaan punainen valo
2c	Odotus	Vihreä	Jatka	Havaitaan vihreä valo
3	Jatka	(Ei vaaraa)	Lopetus
4	Lopetus

Tilat Aloitus ja Lopetus ovat kaaviossa vain havainnollisuuden vuoksi.

Yllä oleva tilataulu voidaan helposti ohjelmoida tietokoneelle täysin samanlaisena kuin miten ajajakin toimii. Kaikki ohjelmointikielet ovat keskenään Turing-vahvoja, joten samat asiat voidaan ohjelmoida eri kielillä. Ohjelmoitaessa Prolog on kuitenkin erityisen sopiva sen takia, että Prologin sisäinen semantiikka tukee suoraan tilakaavioiden ohjelmointia. Jokaiselle tilakaavion kentälle ja tekijälle löytyy kielestä suoraan soveltuva rakenne.

Katso myös

• Symbolinen analysointi on yksi lähdekoodin analysointivaihtoehdoista.
• Staattinen analyysi
• Dynaaminen analyysi

Kirjallisuutta

• Boyer, R. S. & Elspas, B. & Levitt, K. N. (1975): SELECT - A formal system for testing and debugging programs by symbolic execution, pages 234-245., Los Angeles, CA.
• Church, A. (1938). A Bibliography of Symbolic Logic, ISBN 0821800841, out of print.
• Cheatham, T. & Holloway, G. & Townley., J. (1979). Symbolic Evaluation and the Analysis of Programs. IEEE Trans. Softw. Eng. 5 (4), 402-417.
• Clarke, L. (1975). A system to generate test data and symbolically execute programs. Rep. No. CU-CS-060-75, Dep. of Computer Sci, U. of Colorado, Colorado.
• Havlak, P. (1994). Interprocedural Symbolic Analysis. . PhD thesis, Dept. of Computer Science, Rice University.
• Harnad, S. (1990) The Symbol Grounding Problem. Physica D 42: 335-346.
• Xie, Y. & Chou, A. & Engler, D. R. (2003). ARCHER: using symbolic, path-sensitive analysis to detect memory access errors. ESEC / SIGSOFT FSE-conference

Aiheesta muualla

Symbolinen analyysi ohjelmien ymmärtämisen teoriana:

• Comparing Static, Dynamic and Symbolic Analysis^{[vanhentunut linkki]} Staattisen, dynaamisen ja symbolisen analyysin filosofinen vertailu (Englanniksi)
• [1]^{[vanhentunut linkki]} Symbolic Analysis and Atomistic Model as a Basis for a Program Comprehension Methodology. Väitöskirja (2008)
• Symbolic Analysis^{[vanhentunut linkki]} Symbolinen analyysi: Web-sivut (Englanniksi)