Formalna semantika programskih jezika

U teoretskom računarstvu, formalna semantika je disciplina koja se bavi rigoroznim matematičkim proučavanjem značenja programskih jezika i modela računanja.

Formalna semantika jezika je dana matematičkim modelom koji opisuje moguća računanja koja jezik opisuje.

Postoje mnogi pristupi formalnoj semantici, koji se mogu razvrstati u tri glavna razreda:

• Denotacijska semantika, u kojoj je svaka fraza jezika prevedena u denotaciju, tj. frazu u drugom jeziku. Denotacijska semantika slabo odgovora kompilaciji, iako je "ciljni jezik" obično matematički formalizam mjesto nekog drugog računalnog jezika. Na primjer, denotacijska semantika funkcijskih jezika se često prevodi u teoriju domena;
• Operacijska semantika, u kojoj se izravno opisuje izvršavanje jezika (mjesto prevođenjem). Operacijska semantika slabo odgovora interpretaciji, iako je opet "jezik izgradnje" interpretera općenito matematički formalizam. Operacijska semantika može definirati apstraktni stroj (kao što je SECD stroj) i dati značenje frazama opisujući prelaze koje one induciraju nad stanjima stroja. Alternativno, kao s čistim lambda računom, operacijska semantika može biti definirana sintaksnim pretvorbama nad frazama samog jezika;
• Aksiomatska semantika, u kojo j se značenje daje frazama opisujući logičke aksiome koji se na njih primjenjuju. Aksiomatska semantika ne razlikuje značenje fraze i logičkih formula koji je opisuju; njezino značenje jest točno ono što o njoj može biti dokazano u nekoj logici. Kanonski primjer aksiomatske semantike jest Hoareova logika.

Razlika između triju širokih razreda pristupa može nekad izgledati mutna, ali svi poznati pristupi formalnoj semantici koriste gornje tehnike, ili neku njihovu kombinaciju.

Osim izbora između denotacijskog, operacijskog i aksiomatskog pristupa, većina varijacija u sustavima formalne semantike izniče iz izbora podržavajućeg matematičkog formalizma.

Područje proučavanja formalne semantike uključuje sljedeće:

• definiciju semantičkih modela
• odnose između različitih semantičkih modela
• odnose između različitih pristupa značenju, i
• odnose između računanja i temeljnih matematičkih struktura iz polja kao što su logika, teorija skupova, teorija modela, teorija kategorija itd.

Usko je povezana s drugim područjima računarstva, kao što su dizajniranje programskih jezika, teorija tipova, jezični procesori i interpreteri, verifikacija programa i provjera modela.

Vanjske poveznice

• Semantics with Applications
• The Computer Science behind ToonTalk

Izvori

• Shriram Krishnamurthi. Programming Languages: Application and Interpretation. (dostupno besplatno na Webu, kao PDF)
• John C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. (ISBN 0-521-59414-6)
• Carl Gunter. Semantics of Programming Languages. MIT Press, 1992. (ISBN 0-262-07143-6)
• Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993 (paperback ISBN 0-262-73103-7)