A programozás szemantikája egy olyan tudományág, amely a programnyelvi konstrukciók jelentéseinek formalizálását vizsgálja formális matematikai modelljeik felépítésével . Az ilyen modellek felépítéséhez különféle eszközök használhatók, például matematikai logika , λ-számítás , halmazelmélet , kategóriaelmélet , modellelmélet , univerzális algebra . A programozási nyelv szemantikájának formalizálása felhasználható mind a nyelv leírására, mind a nyelv tulajdonságainak meghatározására, mind pedig formális ellenőrzés céljából.programokat ezen a programozási nyelven.
A nyelv szemantikája a szavak szemantikai jelentése. A programozásban az operátorok kezdeti szemantikai jelentése , az alapvető nyelvi konstrukciók stb.
Példa:
Első kód: i=0; while(i<5){i++;} Második kód: i=0; do{i++;} while(i<=4);Logikusan ez a két kódrészlet ugyanazt csinálja, munkájuk eredménye azonos. Ugyanakkor szemantikailag ez két különböző ciklus . Címkék is:
<i></i> <em></em>pontosan ugyanúgy fog kinézni az oldalon, vagyis valójában ugyanazt ábrázolják, és szemantikailag az első címke dőlt, a második pedig a logikai kijelölés (a böngészők dőlt betűvel jelennek meg).
A műveleti szemantika a nyelv szintaktikai fogalmaihoz használatos . A függvényeket jól formált szöveges definíciókként kezeli, amelyek egy érvre alkalmazhatók, nem pedig a kifejezés matematikai értelmében vett függvényekként.
A műveleti szemantika különböző típusait osztályozzák:
Axiomatikus szemantika – A nyelv minden szintaktikai konstrukciójának szemantikája axiómák vagy következtetési szabályok halmazaként definiálható, amelyek segítségével következtetni lehet az adott konstrukció eredményeire. Az egész program jelentésének megértéséhez ezeket az axiómákat és a következtetési szabályokat ugyanúgy kell használni, mint a közönséges matematikai tételek bizonyításakor. Feltételezve, hogy a bemeneti változók értékei eleget tesznek bizonyos megszorításoknak, az axiómák és a következtetési szabályok felhasználhatók más változók értékeinek megszorítására az egyes programutasítások végrehajtása után. A program végrehajtása során igazolást kapunk arról, hogy a számított eredmények megfelelnek a bemeneti értékekhez viszonyított értékükre vonatkozó szükséges korlátozásoknak. Ez azt jelenti, hogy a kimenet bizonyítottan a megfelelő függvény értékeit képviseli, ami a bemenet értékeiből számítható ki.
A denotációs szemantika a valós matematikai objektumokat a programban szereplő kifejezésekkel állítja összefüggésbe, vagyis a kifejezések jelölik (azaz a kifejezések jelölik – ahonnan a „ denotational ”) értékeiket [1 ] . A denotációs szemantika felépítésében a legfontosabb, köztük úttörő eredményeket D. Scott (Dana Scott) és K. Strachey (Christopher Strachey) munkáiban szerezték meg az 1960-as évek végén és az 1970-es évek elején az Oxfordi Egyetemen [2] . Scott volt az első, aki megépítette a λ-kalkulus modelljét a teljes, részben rendezett halmaz koncepciója alapján. Ehhez olyan függvényeket használt, amelyek egy ilyen halmazon folyamatosak.
Az értelmező szemantika a konstrukciók működési szemantikáját írja le alacsony szintű programozási nyelvek ( asseller nyelv , gépi kód ) szempontjából. Ez a módszer lehetővé teszi a program lassan futó szakaszainak azonosítását, és gyakran használják a programozási rendszerek megfelelő töredékeiben a programkód optimalizálása érdekében .
A fordítási szemantika a konstrukciók működési szemantikáját írja le magas szintű programozási nyelvek szempontjából . Ezzel a módszerrel a programozó által már ismert nyelvhez hasonló nyelvet tanulhat meg.
A transzformációs szemantika a nyelvi konstrukciók műveleti szemantikájának leírása ugyanazon nyelv szempontjából. A transzformációs szemantika a metaprogramozás alapja .
Folyamatos érdeklődés és kutatás tárgya a helyességet, illetve a programok helyességét bizonyító rendszerek felépítése. A funkcionális programok helyességét igazoló bizonyító rendszerek bizonyultak a legfejlettebbnek, amelyek Robin Milner LCF rendszerére , valamint R. Boyer (R. Boyer) és J. Moore (J. Moore) rendszerére nyúlnak vissza. .
A jelenlegi kutatások a konstruktív logikán alapuló rendszerek felépítésére és a programok és a bizonyítások közötti analógia megteremtésére irányulnak. Lényeges, hogy mind a programok, mind a bizonyítások belemerültek egy típusokkal rendelkező λ-számításba, amely magasabb rendű formális rendszer. Ez biztosítja, hogy csak a megszűnő programok építhetők fel. Az egyik ilyen rendszer a Coq rendszer .