A programozási nyelvek elméletében a szemantika a programnyelvek jelentésének szigorú matematikai-logikai vizsgálata. A szemantika azt határozza meg, hogy az adott nyelv szintaxisának megfelelő karakterláncok milyen számítási jelentéssel bírnak. Ez a terület szorosan összefügg a matematikai bizonyítások szemantikájával, és gyakran átfedés is van közöttük.

A szemantika leírja, hogy egy adott nyelven írt program milyen lépéseken keresztül hajtódik végre a számítógépen. Ez történhet úgy, hogy megadjuk a bemenet és kimenet közötti kapcsolatot, vagy úgy, hogy részletesen elmagyarázzuk, hogyan fut le a program egy adott platformon — ezáltal egyfajta számítási modellt hozunk létre.

Történelme 1967-ben Robert W. Floyd publikálta az „Assigning meanings to programs” című tanulmányát, amelynek fő célja az volt, hogy szigorú szabványt alkosson a számítógépes programokkal kapcsolatos bizonyításokhoz, beleértve a helyesség, ekvivalencia és terminálás (azaz a program befejeződésének) igazolását. „A programozási nyelv szemantikai definíciója a mi megközelítésünkben a szintaktikai definícióra épül. Meg kell határoznia, hogy a szintaktikailag helyes program mely kifejezései számítanak utasításnak, és milyen feltételeket kell teljesítenie az értelmezésnek az egyes utasítások környezetében.”

1969-ben Tony Hoare publikált egy tanulmányt a Hoare-logikáról, amely Floyd elképzeléseire épült, és ma már gyakran együtt említik őket axiomatikus szemantikaként.

Az 1970-es években jelentek meg a operációs szemantika és a denotációs szemantika fogalmai, amelyek különböző módon írják le a programok jelentését.

Áttekintés A formális szemantika területe magában foglalja a következőket:

A szemantikai modellek definiálása A különböző szemantikai modellek közötti kapcsolatok vizsgálata Eltérő jelentésértelmezési megközelítések összehasonlítása A számítás és az alapul szolgáló matematikai struktúrák közötti kapcsolat olyan területekről, mint a logika, a halmazelmélet, a modellelmélet, a kategóriaelmélet stb.

A formális szemantika szoros kapcsolatban áll a számítástechnika más területeivel, mint például a típuselmélet, a programozási nyelvek tervezése, a fordítóprogramok és interpreterek, a programverifikáció és a modellellenőrzés.

Megközelítések Többféle megközelítés is létezik a formális szemantika területén, ezek 3 nagy kategóriába sorolhatók:

Denotációs szemantika Ebben a megközelítésben a nyelv minden kifejezése egy denotációval, azaz egy elvont jelentéssel van összekapcsolva. Ezek a denotációk gyakran matematikai objektumok, amelyek egy matematikai térben helyezkednek el — bár ez nem feltétel. A gyakorlatban a denotációkat matematikai jelöléssel írják le, amelyet egy denotációs metanyelv formalizálhat. Például a funkcionális nyelvek denotációs szemantikája gyakran doménelméletre fordítja a nyelvet. A denotációs leírások kompozíciós fordításként is szolgálhatnak, és alapul szolgálnak fordítók tervezéséhez.

Operációs szemantika Ez a megközelítés a nyelv végrehajtását közvetlenül írja le, nem fordítással. Lazán megfeleltethető az értelmezésnek (interpretálásnak), bár az értelmező „nyelve” itt is matematikai formalizmus. Az operációs szemantika gyakran definiál egy absztrakt gépet (pl. SECD-gép), és a kifejezések jelentését az alapján adja meg, hogy milyen állapotváltozásokat idéznek elő. Alternatív megközelítésként — például a lambda-kalkulusban — a szemantika szintaktikai transzformációkkal is leírható.

Axiomatikus szemantika Ebben az esetben a kifejezések jelentését azokra vonatkozó axiómák írják le. Nem különül el a kifejezés jelentése attól, amit logikai formulákkal bizonyítani lehet róla — a jelentés pontosan az, amit egy adott logikában bizonyítani tudunk. A legismertebb példa az axiomatikus szemantikára a Hoare-logika.

A denotációs, operációs és axiomatikus megközelítések mellett a formális szemantikai rendszerek közötti különbségek leginkább abban rejlenek, milyen matematikai formalizmust használnak háttérként.

A formális szemantika néhány változata: Akcióalapú szemantika A denotációs szemantikát modularizálja, makro- és mikroszintű jelentésekre bontva. Előre definiált szemantikai entitásokat használ, mint például „akciók”, „adatok” és „eredménygenerálók”. Algebrai szemantika Az axiomatikus szemantika egyik formája, amely algebrai törvények segítségével írja le a programok jelentését. Támogatja a denotációs és operációs szemantikát is, és lehetővé teszi a programok formális levezetését. Attribútumgrammatikák Olyan rendszerek, amelyek a nyelvi szintaxishoz metaadatokat (attribútumokat) rendelnek. Gyakran használják kódgenerálásra és a grammatikák kibővítésére. Kategóriaelméleti (funktoriális) szemantika A kategóriaelméletet alkalmazza matematikai formalizmusként. Az axiomatikus szemantikával áll kapcsolatban, és szintaktikai reprezentációkat biztosít a jelentéshez. Párhuzamos szemantika A konkurens számításokat írja le, például az aktormodell vagy a folyamatkalkulusok segítségével. Játékelméleti szemantika A játékelmélet metaforáit használja a programok jelentésének modellezésére. A program és a környezet közötti interakciót játékos formában írja le. Predikátumtranszformációs szemantika Edsger W. Dijkstra nevéhez fűződik. A program jelentését úgy írja le, mint egy függvényt, amely egy utófeltételt alakít át a hozzá tartozó előfeltétellé.

Kapcsolatok leírása szemantikák között Számos okból lehet indokolt, hogy leírjuk a különböző formális szemantikák közötti kapcsolatokat. Például:

Bizonyítható, hogy egy adott nyelvhez tartozó operációs szemantika kielégíti az axiomatikus szemantika logikai formuláit. Egy ilyen bizonyítás azt mutatja meg, hogy megbízható (sound) az adott operációs értelmezési stratégia, ha az axiomatikus bizonyítási rendszerrel érvelünk róla. Bizonyítható, hogy egy magas szintű absztrakt géphez tartozó operációs szemantika szimulációs kapcsolatban áll egy alacsonyabb szintű gép szemantikájával. Ebben az esetben az alacsony szintű gép primitívebb műveleteket tartalmaz, mint a magas szintű definíció. Egy ilyen bizonyítás igazolja, hogy az alacsony szintű gép hűen megvalósítja a magas szintű gépet.

Emellett lehetőség van arra is, hogy több szemantikát absztrakciókon keresztül kapcsoljunk össze, például az absztrakt interpretáció elméletének segítségével.

Lásd még Formális szemantika (logika) Ontológia Ontológia (informatika)

Fordítás

Források

Goguen, J. A. (1975). Semantics of computation. In *Category Theory Applied to Computation and Control* (Lecture Notes in Computer Science, Vol. 25, pp. 151–163). Springer. https://doi.org/10.1007/3-540-07142-3_75 Floyd, R. W. (1967). Assigning Meanings to Programs. In J. T. Schwartz (Ed.), *Mathematical Aspects of Computer Science* (Vol. 19, pp. 19–32). American Mathematical Society. Knuth, D. E. Memorial Resolution: Robert W. Floyd (1936–2001). Stanford University Faculty Memorials. Hoare, C. A. R. (1969). An axiomatic basis for computer programming. *Communications of the ACM*, 12(10), 576–580. https://doi.org/10.1145/363235.363259 Winskel, G. (1993). *The formal semantics of programming languages: An introduction*. MIT Press. Schmidt, D. A. (1986). *Denotational Semantics: A Methodology for Language Development*. William C. Brown Publishers. Plotkin, G. D. (1981). A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University. Goguen, J. A., Thatcher, J. W., Wagner, E. G., & Wright, J. B. (1977). Initial algebra semantics and continuous algebras. *Journal of the ACM*, 24(1), 68–95. https://doi.org/10.1145/321992.321997 Mosses, P. D. (1996). Theory and practice of action semantics. BRICS Report RS9653, Aarhus University. Deransart, P., Jourdan, M., & Lorho, B. (1988). *Attribute Grammars: Definitions, Systems and Bibliography*. Lecture Notes in Computer Science 323, Springer-Verlag. Lawvere, F. W. (1963). Functorial semantics of algebraic theories. *PNAS*, 50(5), 869–872. https://doi.org/10.1073/pnas.50.5.869 Tarlecki, A., Burstall, R. M., & Goguen, J. A. (1991). Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories. *Theoretical Computer Science*, 91(2), 239–264. https://doi.org/10.1016/0304-3975(91)90085-G Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., & Sewell, P. (2015). The problem of programming language concurrency semantics. In *European Symposium on Programming Languages and Systems* (pp. 283–307). Springer. https://doi.org/10.1007/978-3-662-46669-8_12 Abramsky, S. (2009). Semantics of interaction: An introduction to game semantics. In A. M. Pitts & P. Dybjer (Eds.), *Semantics and Logics of Computation* (pp. 1–32). Cambridge University Press. https://doi.org/10.1017/CBO9780511526619.002 Dijkstra, E. W. (1975). Guarded commands, nondeterminacy and formal derivation of programs. *Communications of the ACM*, 18(8), 453–457. https://doi.org/10.1145/360933.360975

Irodalom Floyd, R. W. (1967). Assigning Meanings to Programs. In J. T. Schwartz (Ed.), Mathematical Aspects of Computer Science (Vol. 19, pp. 19–32). American Mathematical Society. Hennessy, M. (1990). The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley. Tennent, R. D. (1991). Semantics of Programming Languages. Prentice Hall. Gunter, C. (1992). Semantics of Programming Languages. MIT Press. Nielson, H. R., & Nielson, F. (1992). Semantics With Applications: A Formal Introduction. Wiley. . (Archivált PDF-verzió: 2012.04.17.) Winskel, G. (1993). The Formal Semantics of Programming Languages: An Introduction. MIT Press. Mitchell, J. C. (1995). Foundations for Programming Languages. (Postscript formátumban elérhető.) Slonneger, K., & Kurtz, B. L. (1995). Formal Syntax and Semantics of Programming Languages. Addison-Wesley. Reynolds, J. C. (1998). Theories of Programming Languages. Cambridge University Press. Harper, R. (2006). Practical Foundations for Programming Languages. (Archivált PDF-verzió: 2007.06.27.) Nielson, H. R., & Nielson, F. (2007). Semantics with Applications: An Appetizer. Springer. Stump, A. (2014). Programming Language Foundations. Wiley. Krishnamurthi, S. (2012). Programming Languages: Application and Interpretation (2. kiadás) Winskel, G. Denotational Semantics. Egyetemi jegyzet, University of Cambridge. (PDF formátumban elérhető)

További információk Semantics.

Kategória:Programozási nyelvek