Mittestandardsed programmeerimiskeelte semantikad

Standardseks loetakse semantikat, mis kirjeldab programmi tegevust enam-vähem vastavalt reaalsele protsessile. Lubatud on detailidest abstraheerimine. Sellest hälbiv semantika on mittestandardne. Kuid ka sellistel on praktilisi rakendusi. Näiteks mitmesugused kogumissemantikad on kasulikud programmianalüüside korrektsuse näitamisel. Härmel Nestra on oma teadustöös uurinud transfiniitseid semantikaid, mis kujutavad programmide tööd jätkuvana pärast lõpmatut tsüklit. Selliste semantikate rakendused on selliste programmiteisendajate korrektsuse näitamisel, mis eemaldavad või vahetavad koodiosi nii, et lõpmatu tsükkel võib asenduda normaalselt lõpetava koodiga.

Uurida võib, millised transfiniitsed semantikad on mainitud rakenduste jaoks sobivad erinevate programmikonstruktsioonide olemasolul (nt tõenäosuslikult töötavad käsud, mitmelõimelisus, rekursioon). Tegu on klassikalises mõttes puhtteoreetilise valdkonnaga. Sobib eelkõige kraadiõppe tudengile, kellele meeldib matemaatika ja soovib programmeerimisele vaadata läbi matemaatika prisma.

Non-standard semantics

Standard semantics attempt to capture the real-world behaviour of the program. We may allow some abstractions and approximations, but the idea is to stay true to the original meaning of the program. Non-standard semantics deliberately deviate and ascribe peculiar meanings to programs, meanings that are nevertheless useful for specific applications. In order to prove the correctness of static analyzers or program slicers, so called collecting semantics are used; these collect the set of all possible program states that may reach a given program point. Härmel Nestra has conducted research into transfinite semantics, which conceive programs as continuing execution beyond infinite loops! This is critical to prove the correctness of program transformations, such as slicing, that may eliminate non-terminating loops from the program.

In this context, you may explore which transfinite semantics can be used to prove the correctness of such transformations in the presence of various programming constructs, such as probabilistic statements, multi-threading, and recursion. This is a purely theoretical exploration and is well-suited to students who like mathematics and would like to view programming through a mathematical lens.

Contact: Härmel Nestra