Inom datavetenskap är denotationell semantik (ibland kallad matematisk semantik eller Scott–Strachey-semantik) en metod för att formellt beskriva betydelsen av programmeringsspråk. Metoden bygger på att program och programuttryck tilldelas matematiska objekt, kallade denotationer, som representerar deras betydelse.
Denotationell semantik är en av de tre klassiska angreppssätten inom formell semantik för programmeringsspråk, vid sidan av operationell semantik och axiomatisk semantik.
Ett centralt krav inom denotationell semantik är att semantiken ska vara kompositionell: betydelsen av ett sammansatt programuttryck ska bestämmas entydigt av betydelsen hos dess deluttryck.
Översikt Grundidén i denotationell semantik är att tolka program som matematiska funktioner eller andra abstrakta strukturer. Till exempel kan:
uttryck tolkas som funktioner från en omgivning (miljö) till värden, program tolkas som funktioner från indata till utdata, icke-terminerande beräkningar representeras med särskilda bottenelement (⊥).
För att kunna modellera rekursion och potentiellt oändliga beräkningar används ofta domänteori, där betydelser beskrivs med partiellt ordnade mängder och fixpunkter.
Historik Denotationell semantik utvecklades under slutet av 1960-talet och början av 1970-talet, främst genom arbeten av Dana Scott och Christopher Strachey. Deras mål var att ge programmeringsspråk en exakt matematisk grund som var oberoende av hur program faktiskt exekveras på en dator.
Scott introducerade användningen av kontinuerliga funktioner över fullständigt partiellt ordnade mängder (CPO:er) för att hantera rekursion på ett matematiskt välgrundat sätt. Detta lade grunden för modern domänteori och denotationell semantik.
Grundläggande begrepp Domäner En domän är ett matematiskt objekt som representerar möjliga värden av ett uttryck eller ett program. Domäner innehåller ofta ett särskilt element ⊥ som representerar icke-terminering eller odefinierade beräkningar.
Miljöer Betydelsen av ett programuttryck definieras ofta relativt en miljö, som anger vilka värden fria variabler har. Semantiken blir då en funktion från miljöer till värden i en domän.
Fixpunkter Rekursiva definitioner ges betydelse genom minsta fixpunkter av funktioner på domäner. Detta gör det möjligt att formellt definiera funktioner som till exempel fakultet eller rekursiva loopar.
Exempel Ett aritmetiskt uttryck som n * m tolkas i denotationell semantik som en funktion som, givet en miljö där n och m har värden, returnerar produkten av dessa värden.
Rekursiva funktioner konstrueras som gränsvärden av successivt mer definierade approximationer, vilket säkerställer att betydelsen är matematiskt väldefinierad.
Utvidgningar Denotationell semantik har vidareutvecklats för att hantera mer avancerade språkegenskaper, såsom:
konkurrens och parallellism, icke-determinism, undantagshantering, lokalt tillstånd och imperativa konstruktioner, polymorfism och avancerade typsystem.
I vissa fall används alternativa matematiska ramverk, till exempel kategoriteori och spelbaserad semantik.
Relation till andra semantiska metoder Denotationell semantik skiljer sig från:
operationell semantik, som beskriver program genom exekveringssteg, axiomatisk semantik, som beskriver program genom logiska egenskaper och bevis.
En viktig forskningsfråga är i vilken utsträckning denotationell och operationell semantik sammanfaller, särskilt vad gäller full abstraktion.
Betydelse och användning Denotationell semantik används främst inom:
teoretisk datavetenskap, utveckling och analys av programmeringsspråk, formell verifiering och programsäkerhet, undervisning i programmeringsspråksteori vid universitet och högskolor.
Metoden ger ett kraftfullt verktyg för att resonera matematiskt om programs korrekthet och egenskaper, oberoende av implementation.
Referenser
Vidare läsning
Externa länkar
Kategori:Datavetenskap