Semantik i programmering är en disciplin som studerar formaliseringen av betydelsen av programmeringsspråkskonstruktioner genom att bygga deras formella matematiska modeller . Olika verktyg kan användas som verktyg för att bygga sådana modeller, till exempel matematisk logik , λ-kalkyl , mängdlära , kategoriteori , modellteori , universell algebra . Formaliseringen av semantiken för ett programmeringsspråk kan användas både för att beskriva språket, för att bestämma språkets egenskaper och i syfte att formell verifiering av program på detta programmeringsspråk.
Ett språks semantik är den semantiska betydelsen av ord. I programmering, den initiala semantiska betydelsen av operatorer , grundläggande språkkonstruktioner, etc.
Exempel:
Första koden: i=0; while(i<5){i++;} Andra koden: i=0; gör{i++;} while(i<=4);Logiskt sett gör dessa två kodfragment samma sak, resultaten av deras arbete är identiska. Samtidigt, semantiskt, är dessa två olika cykler . Taggar också:
<i></i> <em></em>kommer att se exakt likadant ut på sidan, det vill säga att de faktiskt representerar samma sak, och semantiskt är den första taggen kursiv och den andra är logisk markering (webbläsare visas i kursiv stil).
Operationell semantik används för språkets syntaktiska begrepp . Den behandlar funktioner som textuella välformade definitioner som ger tillämpning på ett argument, och inte som funktioner i termens matematiska mening.
Det finns en klassificering av olika typer av operativ semantik:
Axiomatisk semantik - Semantiken för varje syntaktisk konstruktion i ett språk kan definieras som en uppsättning axiom eller slutledningsregler som kan användas för att härleda resultatet av den konstruktionen. För att förstå innebörden av hela programmet bör dessa axiom och slutledningsregler användas på samma sätt som i beviset för vanliga matematiska satser. Förutsatt att värdena för indatavariablerna uppfyller vissa begränsningar, kan axiomen och slutledningsreglerna användas för att erhålla begränsningar på värdena för andra variabler efter exekveringen av varje programsats. När programmet körs får vi ett bevis på att de beräknade resultaten uppfyller de nödvändiga begränsningarna för deras värden i förhållande till ingångsvärdena. Det vill säga att utgången har visat sig representera värdena för motsvarande funktion beräknad från ingångens värden.
Denotationssemantik sätter verkliga matematiska objekt i överensstämmelse med uttryck i programmet , det vill säga uttryck betecknar ( eng . att beteckna - varifrån "denotational") deras värden [1] . De viktigaste, inklusive banbrytande, resultat i konstruktionen av denotationssemantik erhölls i verk av D. Scott (Dana Scott) och K. Strachey (Christopher Strachey) i slutet av 1960-talet och början av 1970-talet vid Oxford University [2] . Scott var den första som byggde en modell av λ-kalkylen baserad på konceptet med en komplett, delvis ordnad uppsättning. För att göra detta använde han funktioner som är kontinuerliga på en sådan uppsättning.
Tolkande semantik är en beskrivning av den operativa semantiken för konstruktioner i termer av programmeringsspråk på låg nivå ( assemblerspråk , maskinkod ). Denna metod låter dig identifiera långsamt exekverande avsnitt av programmet och används ofta i motsvarande fragment av programmeringssystem för att optimera programkoden .
Translationell semantik är en beskrivning av den operativa semantiken för konstruktioner i termer av programmeringsspråk på hög nivå . Med den här metoden kan du lära dig ett språk som liknar det som programmeraren redan känner till.
Transformationell semantik är en beskrivning av den operativa semantiken för språkkonstruktioner i termer av samma språk. Transformationell semantik är grunden för metaprogrammering .
Ämnet för ständigt intresse och forskning är konstruktionen av system för att bevisa riktigheten, eller riktigheten av program. Bevissystemen för fallet med korrektheten av funktionella program visade sig vara de mest utvecklade, som går tillbaka till Robin Milners LCF-system och R. Boyers (R. Boyer) och J. Moores (J. Moore) system . .
Aktuell forskning är inriktad på att bygga system baserade på konstruktiv logik och att etablera en analogi mellan program och bevis. Det är betydelsefullt att både program och bevis anses vara nedsänkta i en λ-kalkyl med typer, vilket är ett formellt system av högre ordning. Detta säkerställer att endast program som avslutas kan byggas. Ett sådant system är Coq- systemet .