See veebileht kasutab küpsiseid kasutaja sessiooni andmete hoidmiseks. Veebilehe kasutamisega nõustute ETISe kasutustingimustega. Loe rohkem
Olen nõus
"Eesti Teadusfondi uurimistoetus" projekt ETF7543
ETF7543 "Mittestandardsed programmeerimisekeelte semantikad (1.01.2008−31.12.2012)", Härmel Nestra, Tartu Ülikool, Matemaatika-informaatikateaduskond.
ETF7543
Mittestandardsed programmeerimisekeelte semantikad
Non-Standard Semantics of Programming Languages
1.01.2008
31.12.2012
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)50,0
4. Loodusteadused ja tehnika4.4. MatemaatikaP110 Matemaatiline loogika, hulgateooria, kombinatoorika1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)50,0
PerioodSumma
01.01.2008−31.12.2008180 000,00 EEK (11 504,10 EUR)
01.01.2009−31.12.2009172 800,00 EEK (11 043,93 EUR)
01.01.2010−31.12.2010139 794,00 EEK (8 934,46 EUR)
01.01.2011−31.12.20118 934,00 EUR
40 416,49 EUR

Kavas on jätkata teoreetilisi uurimusi imperatiivsete keelte semantikate alal suunas, mida on juba arendatud H. Nestra teaduspublikatsioonides aastatest 2004--2006. Jätkuvalt on motivatsiooniks leida semantikaid, mis oleksid sobivaks vahendiks kirjeldamaks slitseerimise korrektsust. Standardsete semantikate kasutamisel slitseerimise formaliseerimiseks ilmneb nn semantiline anomaalia. See nähtus võib ilmneda, kui teisendamisel eemaldatakse lõpmatu tsükkel ja tulemuseks olev programm jõuab täitmisega originaalprogrammist kaugemale. Üks lähenemine semantilisest anomaaliast ülesaamisel on transfiniitsete semantikate kasutamine. Transfiniitse semantika järgi kuuluvad programmi semantikasse ka kujutletavad operatsioonid pärast lõpmatut tsüklit. H. Nestra töödes aastatest 2004--2005 ja doktoritöös on välja arendatud keelest sõltumatu matemaatiline raamistik transfiniitsete semantikate kirjeldamiseks ja tõestatud selles kahe standardse slitseerimisalgoritmi korrektsus teatavate transfiniitsete semantikate klassi suhtes. Alguse on see suund saanud P. Cousot' jt töödes juba mõned aastad varem. Transfiniitse semantika kasutamisele seab piirid see, et programmide töö vahetulemuste nummerdamiseks kasutatakse ordinaale. See on võimalik lõpmatute tsüklite puhul, kuid lõpmatu sügavusega rekursiooni korral mitte. H. Nestra artiklis aastast 2006 pakutakse uue uurimissuunana välja murdsemantikad, mis üldistavad transfiniitset semantikat ja on kasutatavad ka rekursiooni puhul. Järgnevate aastate jooksul on kavas murdsemantikaid edasi uurida. Loodame leida murdsemantikaid, mille kasutamisel oleksid väiksemad kitsendused kui varemkirjeldatute puhul. Arendame välja murdsemantikate esituse teatavate operaatorite suurima püsipunkti kaudu sarnaselt standardsete semantikatega. Vähima või suurima püsipunkti kaudu esitatud semantikaid on võimalik asetada nn Cousot' hierarhiasse, mis näitab semantika abstraktsusastet. Tõenäoliselt osutub, et murdsemantikad on vastavatest jälitussemantikatest konkreetsemad, kuid puusemantikatest abstraktsemad. Kavas on uurida ka programmianalüüsis kasutatavaid semantikaid, mh seoses Cousot' hierarhiaga. Lisaks imperatiivsete keelte semantikatele on kavas paralleelselt uurida ka funktsionaalsete ja loogiliste keelte semantikaid.
We plan to continue research on theory of semantics of imperative programming languages in the direction developed by H. Nestra in 2004--2006. The motivation is still to find semantics that would be appropriate for handling correctness of program slicing. When using standard semantics for formalizing the concept of program slicing, a phenomenon called semantic anomaly arises. This can appear if an infinite loop is omitted from the program and the resulting program reaches farer in the code than the original program when they are executed. One approach for overcoming semantic anomaly is using transfinite semantics. According to transfinite semantics, the meaning of program contains also imaginary operations performed after infinite loops. In the works by H. Nestra from 2004--2005 and his PhD thesis, a mathematical framework independent from programming language is developed for describing transfinite semantics and correctness of two standard slicing algorithms w.r.t. a class of transfinite semantics is proven in this framework. This approach of research has started in the works of P. Cousot and others already some years earlier. Using transfinite semantics is limited by the fact that ordinals are used for enumerating the intermediate steps of program execution. This is acceptable in the case of infinite loops but not in the case of infinitely deep recursion. In the paper by H. Nestra from 2006, fractional semantics are proposed as a new approach. Fractional semantics generalize transfinite semantics and are usable also in the case of recursion. During the following years, we plan to investigate fractional semantics further. We hope to find fractional semantics that would require smaller restrictions than the ones described before. We describe fractional semantics similarly to standard semantics via greatest fixpoints of some operators. Semantics represented as least or greatest fixpoints can be inserted to Cousot's hierarchy which indicates the abstractness level of semantics. It probably turns out that fractional semantics are more concrete than the corresponding trace semantics but more abstract than the corresponding tree semantics. We plan to investigate also semantics used in program analysis. Additionally to the semantics of imperative languages, we will start research on semantics of functional and logic programs.