Ohjelmoinnin semantiikka on tieteenala, joka tutkii ohjelmointikielen konstruktien merkityksen formalisointia rakentamalla niiden muodollisia matemaattisia malleja . Tällaisten mallien rakentamisen työkaluina voidaan käyttää erilaisia työkaluja , esimerkiksi matemaattista logiikkaa , λ-laskentaa , joukkoteoriaa , kategoriateoriaa , malliteoriaa , universaalia algebraa . Ohjelmointikielen semantiikan formalisointia voidaan käyttää sekä kielen kuvaamiseen, kielen ominaisuuksien määrittämiseen että ohjelmien muodolliseen varmentamiseen tällä ohjelmointikielellä.
Kielen semantiikka on sanojen semanttinen merkitys. Ohjelmoinnissa operaattoreiden alkuperäinen semanttinen merkitys , peruskielikonstruktiot jne.
Esimerkki:
Ensimmäinen koodi: i = 0; while(i<5){i++;} Toinen koodi: i = 0; do{i++;} while(i<=4);Loogisesti nämä kaksi koodinpätkää tekevät saman asian, heidän työnsä tulokset ovat identtiset. Samanaikaisesti semanttisesti nämä ovat kaksi eri sykliä . Myös tunnisteet:
<i></i> <em></em>näyttävät sivulla täsmälleen samalta, eli ne edustavat itse asiassa samaa asiaa, ja semanttisesti ensimmäinen tunniste on kursivoitu ja toinen on looginen valinta (selaimet näyttävät kursiivilla).
Operatiivista semantiikkaa käytetään kielen syntaktisissa käsitteissä . Se käsittelee funktioita tekstimuotoisina hyvin muotoiltuina määritelminä, jotka tarjoavat sovelluksen argumentille, eikä funktioina termin matemaattisessa merkityksessä.
On olemassa luokitus erityyppisille toiminnallisille semantiikkaille:
Aksiomaattinen semantiikka - Jokaisen kielen syntaktisen rakenteen semantiikka voidaan määritellä joukoksi aksioomeja tai päättelysääntöjä, joita voidaan käyttää kyseisen rakenteen tulosten päättämiseen. Koko ohjelman merkityksen ymmärtämiseksi näitä aksioomia ja päättelysääntöjä tulee käyttää samalla tavalla kuin tavallisten matemaattisten lauseiden todistuksessa. Olettaen, että syöttömuuttujien arvot täyttävät joitain rajoituksia, aksioomien ja päättelysääntöjen avulla voidaan saada rajoituksia muiden muuttujien arvoille kunkin ohjelmalausekkeen suorittamisen jälkeen. Kun ohjelma suoritetaan, saamme todisteen siitä, että lasketut tulokset täyttävät tarvittavat rajoitukset niiden arvoille suhteessa syöttöarvoihin. Eli ulostulon on todistettu edustavan vastaavan funktion arvoja, jotka on laskettu tulon arvoista.
Denotaatiosemantiikka asettaa todelliset matemaattiset objektit vastaamaan ohjelman lausekkeita , eli lausekkeet osoittavat ( eng . to denote – mistä "denotational") arvonsa [1] . Tärkeimmät, mukaan lukien uraauurtavat, tulokset denotaatiosemantiikan rakentamisessa saatiin D. Scottin (Dana Scott) ja K. Stracheyn (Christopher Strachey) töissä 1960-luvun lopulla ja 1970-luvun alussa Oxfordin yliopistossa [2] . Scott oli ensimmäinen, joka rakensi mallin λ-laskusta, joka perustui täydellisen osittain tilatun sarjan käsitteeseen. Tätä varten hän käytti toimintoja, jotka ovat jatkuvia sellaisessa joukossa.
Tulkinnallinen semantiikka on rakennelmien toimintasemantiikan kuvaus matalan tason ohjelmointikielillä ( assemblerikieli , konekoodi ). Tämän menetelmän avulla voit tunnistaa ohjelman hitaasti suoriutuvat osat, ja sitä käytetään usein vastaavissa ohjelmointijärjestelmän osissa ohjelmakoodin optimoimiseksi .
Käännössemantiikka on rakennusten toimintasemantiikan kuvaus korkean tason ohjelmointikielillä . Tällä menetelmällä voit oppia kielen, joka on samanlainen kuin ohjelmoijan jo tuntema kieli.
Transformaatiosemantiikka on kuvaus kielikonstruktioiden operatiivisesta semantiikasta saman kielen kannalta. Transformaatiosemantiikka on metaohjelmoinnin perusta .
Jatkuvan mielenkiinnon ja tutkimuksen aiheena on järjestelmien rakentaminen ohjelmien oikeellisuuden tai oikeellisuuden osoittamiseksi. Kehitetyimmiksi osoittautuivat toiminnallisten ohjelmien oikeellisuuden todistusjärjestelmät, jotka juontavat juurensa Robin Milnerin LCF -järjestelmään sekä R. Boyerin (R. Boyer) ja J. Mooren (J. Moore) järjestelmään. .
Nykyinen tutkimus keskittyy rakentamaan järjestelmiä, jotka perustuvat rakentavaan logiikkaan ja luomaan analogiaa ohjelmien ja todisteiden välille. Merkittävää on, että sekä ohjelmien että todisteiden katsotaan olevan upotettuja tyyppejä sisältävään λ-laskentaan, joka on muodollinen korkeampien asteiden järjestelmä. Tämä varmistaa, että vain päättyviä ohjelmia voidaan rakentaa. Yksi tällainen järjestelmä on Coq - järjestelmä .