Title
Моделовање упитних језика са применама у рефакторисању и оптимизацији кода
Creator
Spasić, Mirko, 1985-, 70463753
Copyright date
2021
Object Links
Select license
Autorstvo-Nekomercijalno 3.0 Srbija (CC BY-NC 3.0)
License description
Dozvoljavate umnožavanje, distribuciju i javno saopštavanje dela, i prerade, ako se navede ime autora na način odredjen od strane autora ili davaoca licence. Ova licenca ne dozvoljava komercijalnu upotrebu dela. Osnovni opis Licence: http://creativecommons.org/licenses/by-nc/3.0/rs/deed.sr_LATN Sadržaj ugovora u celini: http://creativecommons.org/licenses/by-nc/3.0/rs/legalcode.sr-Latn
Language
Serbian
Cobiss-ID
Theses Type
Doktorska disertacija
description
Datum odbrane: 23.03.2021.
Other responsibilities
mentor
Vujošević Janičić, Milena, 1980-, 12942695
član komisije
Mitić, Nenad, 1959-, 12528743
član komisije
Marić, Filip, 1978-, 12931687
član komisije
Gilezan, Silvia, 1959-, 13074279
Academic Expertise
Prirodno-matematičke nauke
Academic Title
-
University
Univerzitet u Beogradu
Faculty
Matematički fakultet
Alternative title
Modeling of query languages and applications in code refactoring and code optimization
Publisher
[М. Спасић]
Format
181 стр.
description
рачунарство - спецификација и верификација софтвера / computer science - software specification and verification
Abstract (sr)
Проблем садржаности упита један је од фундаменталних проблема у рачунар-
ским наукама, иницијално дефинисан за релационе упите. Са растућом популарношћу
SPARQL упитног језика, проблем постаје релевантан и актуелан и у овом новом контексту.
У тези је представљен оригинални приступ решавању овог проблема заснован на сво-
ђењу на задовољивост у логици првог реда. Подржана је садржаност упита узимајући
у обзир RDF схему, а разматра се и релација стапања, као слабија форма садржаности.
Доказана је сагласност и потпуност предложеног приступа на широком спектру језич-
ких конструката. Описана је и његова имплементација, у виду решавача SPECS, чији је
кôд јавно доступан. Представљени су резултати детаљне експерименаталне евалуације
на релевантним скуповима примера за тестирање који показују да је SPECS ефикасан,
и да у поређењу са осталим савременим решавачима истог проблема даје прецизније ре-
зултате у краћем времену, уз бољу покривеност језичких конструката. Једна од примена
моделовања упитних језика може бити и при рефакторисању апликација које присту-
пају базама података. У таквим ситуацијама, врло су честе измене којима се мењају
и упити и кôд на језику у коме се они позивају. Такве промене могу сачувати укупну
еквивалентност кода, док на нивоу појединачних делова еквивалентност не мора бити
одржана. Коришћење алата за аутоматску верификацију еквивалентности рефактори-
саног кода може да дâ гаранцију задржавања понашања програма и од суштинског је
значаја за поуздан развој софтвера. Са том мотивацијом, у тези се разматра и модело-
вање SQL упита у теоријама логике првог реда, којим се омогућава аутоматска провера
еквивалентности C/C++ програма са уграђеним SQL-ом, што је и имплементирано у
виду јавно доступног алата отвореног кода SQLAV.
Abstract (en)
The query containment problem is a very important computer science problem,
originally defined for relational queries. With the growing popularity of the SPARQL query
language, it became relevant and important in this new context, too. This thesis introduces
a new approach for solving this problem, based on a reduction to satisfiability in first order
logic. The approach covers containment under RDF SCHEMA entailment regime, and it can
deal with the subsumption relation, as a weaker form of containment. The thesis proves
soundness and completeness of the approach for a wide range of language constructs. It also
describes an implementation of the approach as an open source solver SPECS. The experimental
evaluation on relevant benchmarks shows that SPECS is efficient and comparing to
state-of-the-art solvers, it gives more precise results in a shorter amount of time, while supporting
a larger fragment of SPARQL constructs. An application of query language modeling can
be useful also along refactoring of database driven applications, where simultaneous changes
that include both a query and a host language code are very common. These changes can
preserve the overall equivalence, without preserving equivalence of these two parts considered
separately. Because of the ability to guarantee the absence of differences in behavior between
two versions of the code, tools that automatically verify code equivalence have great benefits
for reliable software development. With this motivation, a custom first-order logic modeling
of SQL queries is developed and described in the thesis. It enables an automated approach
for reasoning about equivalence of C/C++ programs with embedded SQL. The approach is
implemented within a publicly available and open source framework SQLAV.
Classification
004.655.3SQL(043.3)
004.655.3SPARQL:(043.3)
Type
Tekst
Abstract (sr)
Проблем садржаности упита један је од фундаменталних проблема у рачунар-
ским наукама, иницијално дефинисан за релационе упите. Са растућом популарношћу
SPARQL упитног језика, проблем постаје релевантан и актуелан и у овом новом контексту.
У тези је представљен оригинални приступ решавању овог проблема заснован на сво-
ђењу на задовољивост у логици првог реда. Подржана је садржаност упита узимајући
у обзир RDF схему, а разматра се и релација стапања, као слабија форма садржаности.
Доказана је сагласност и потпуност предложеног приступа на широком спектру језич-
ких конструката. Описана је и његова имплементација, у виду решавача SPECS, чији је
кôд јавно доступан. Представљени су резултати детаљне експерименаталне евалуације
на релевантним скуповима примера за тестирање који показују да је SPECS ефикасан,
и да у поређењу са осталим савременим решавачима истог проблема даје прецизније ре-
зултате у краћем времену, уз бољу покривеност језичких конструката. Једна од примена
моделовања упитних језика може бити и при рефакторисању апликација које присту-
пају базама података. У таквим ситуацијама, врло су честе измене којима се мењају
и упити и кôд на језику у коме се они позивају. Такве промене могу сачувати укупну
еквивалентност кода, док на нивоу појединачних делова еквивалентност не мора бити
одржана. Коришћење алата за аутоматску верификацију еквивалентности рефактори-
саног кода може да дâ гаранцију задржавања понашања програма и од суштинског је
значаја за поуздан развој софтвера. Са том мотивацијом, у тези се разматра и модело-
вање SQL упита у теоријама логике првог реда, којим се омогућава аутоматска провера
еквивалентности C/C++ програма са уграђеним SQL-ом, што је и имплементирано у
виду јавно доступног алата отвореног кода SQLAV.
“Data exchange” service offers individual users metadata transfer in several different formats. Citation formats are offered for transfers in texts as for the transfer into internet pages. Citation formats include permanent links that guarantee access to cited sources. For use are commonly structured metadata schemes : Dublin Core xml and ETUB-MS xml, local adaptation of international ETD-MS scheme intended for use in academic documents.