Vuonna tietojenkäsittelyteoria , muodollinen semantiikka (of ohjelmointikieliä ) on tutkimuksen merkityksen tietokoneohjelmien nähdään matemaattisten objektien .
Kuten kielitieteessä , semantiikka , jota käytetään ohjelmointikielissä , osoittaa linkin merkitsijän , ohjelman ja merkityn, matemaattisen objektin välillä. Matemaattinen objekti riippuu ohjelman tiedettävistä ominaisuuksista.
Semantiikka on myös linkki seuraavien välillä:
Yleisimmät semantiikat, joita käytetään ohjelmointikielen ymmärtämiseen, ovat:
Operatiivisessa semantiikassa ohjelman merkitys on koneen tilasekvenssi, joka suorittaa ohjelman. Toisin sanoen ohjelmaa pidetään tilansiirtojärjestelmän kuvauksena .
Tässä semantiikassa ohjelmat:
a=1; b=0ja
a=1; b=0ovat vastaavia, koska niillä on sama merkitys.
Toisaalta ohjelma:
b=0; a=1ei vastaa niitä. Vaikka lopputulos olisi sama, muuttujien a ja b arvojen osoittaminen ei tapahdu samassa järjestyksessä.
Tämä semantiikka on mahdollista tiivistää tarkkailemalla vain osaa koneen muistista, kuten:
Käynnistämä Christopher Strachey ja Dana Scott , denotational semantiikka on lähestymistapa, jossa matemaattinen funktio nimeltään denotation liittyy kuhunkin ohjelmaan, ja tavallaan edustaa sen vaikutusta, sen merkitys. Tämä toiminto ottaa esimerkiksi muistin tilan ennen suoritusta ja johtaa tilaan suorituksen jälkeen .
Tässä semantiikassa kaikki yllä esitetyt esimerkit operatiivisesta semantiikasta ovat vastaavia, mutta ohjelma:
a=1; b=1;ei vastaa niitä.
Denotation-semantiikassa on useita muunnelmia, joista yksi tunnetuimmista on denotation-semantiikka jatkamisella, joka sen sijaan, että yhdistää ohjelman muistiin muuntavaan toimintoon, yhdistää sen toimintoon, joka muuttaa koneen jatkoa (tulevaisuutta) sen jälkeen, kun ohjelman suorittaminen ja jatkaminen ennen ohjelman suorittamista. Toisin sanoen, jatkoa käyttävä denotationinen semantiikka toimii päinvastoin kuin ohjelma, se tarkastelee käskyn jälkeen tapahtuvaa johtopäätöstä siitä, mitä on tapahduttava ennen tätä ohjetta.
Yksi denotationaalisen semantiikan tärkeistä näkökohdista on sävellysominaisuus : ohjelman denotaatio saadaan yhdistämällä sen osatekijöiden merkinnät.
Aksiomaattisessa semantiikassa ohjelma ei ole muuta kuin muunnin loogisten ominaisuuksien muistin tilasta: jos meillä on p true ennen suoritusta, niin meillä on q true jälkeen. Emme ole enää kiinnostuneita muistin tarkasta tilasta, kunhan tiedämme, onko omaisuus kunnossa.
Jos meitä kiinnostava ominaisuus tietää, ovatko a ja b positiivisia ohjelman suorittamisen jälkeen, kaikki edelliset esimerkit ovat vastaavia siinä mielessä, että riippumatta koneen tilasta ennen ohjelman suorittamista, en-poistuminen pätee. Mitä huomaamme Hoare-logiikassa :
a = 1; b = 0Nämä esimerkit osoittavat, että nämä kolme semantiikkaa eivät ole täysin toisistaan riippumattomia:
Mutta päinvastoin on väärin.
Siten voimme hierarkisoida semantiikan sanomalla, että yksi semantiikka on toisen abstraktio vain ja vain, jos viimeisen kaksi vastaavaa ohjelmaa ovat myös vastaavia ensimmäisessä. Nämä suhteet on virallistettu abstraktin tulkinnan teorialla .
Voimme täydentää tämän hierarkian ( osittainen järjestys ) semanttisilla vastaavuuksilla sijoittamalla identiteetin yläosaan (kaksi ohjelmaa ovat identtisiä vain ja vain, jos ne ovat samanmerkkisiä) ja alareunassa kaikkein karkeinta, jota kutsutaan kaaokseksi. , jossa mikä tahansa ohjelma vastaa muuta ohjelmaa.