Szemantika (programozási nyelvek)

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

• Ez a szócikk részben vagy egészben a Semantics (programming languages) című angol Wikipédia-szócikk fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

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. ISBN 0821867288
• Hennessy, M. (1990). The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley. ISBN 978-0-471-92772-3
• Tennent, R. D. (1991). Semantics of Programming Languages. Prentice Hall. ISBN 978-0-13-805599-8
• Gunter, C. (1992). Semantics of Programming Languages. MIT Press. ISBN 0-262-07143-6
• Nielson, H. R., & Nielson, F. (1992). Semantics With Applications: A Formal Introduction. Wiley. ISBN 978-0-471-92980-2. (Archivált PDF-verzió: 2012.04.17.)
• Winskel, G. (1993). The Formal Semantics of Programming Languages: An Introduction. MIT Press. ISBN 0-262-73103-7
• 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. ISBN 0-201-65697-3
• Reynolds, J. C. (1998). Theories of Programming Languages. Cambridge University Press. ISBN 0-521-59414-6
• 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. ISBN 978-1-84628-692-6
• Stump, A. (2014). Programming Language Foundations. Wiley. ISBN 978-1-118-00747-1
• 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

• Aaby, Anthony. Introduction to Programming Languages [archivált változat] (2004) [archiválás ideje: 2015. június 19.]  Semantics.