20.500.12556/RUL-183257 Formalizacija originalne formulacije Poloniusa Formalization of the Original Formulation of Polonius Naloga zastavi matematično formalizacijo Poloniusa, preverjevalnika izposoj za programski jezik Rust. Posebnost Rusta je njegov sistem tipov, ki prevajalniku z ustreznimi pravili o izposojevanju omogoča zagotavljanje pomnilniške varnosti že v času prevajanja. Trenutna implementacija preverjevalnika izposoj, imenovana NLL, je v nekaterih primerih preveč konzervativna, zato so razvijalci Rusta uvedli novo različico, imenovano Polonius, ki je osnovana na bolj natančni analizi toka podatkov. Polonius sicer nikjer ni uradno definiran, viri o njem so razpršeni, zato je cilj te naloge postaviti matematičen okvir, skozi katerega lahko razumemo to novo različico. Tega se lotimo z uporabo množic in izjav, tako da pravila, ki so bila zastavljena v raznih virih, opišemo s pomočjo predikatov ter pravil sklepanja. Končni izdelek je poenostavljen, vendar formalen opis Poloniusa. This thesis provides a mathematical formalization of Polonius, the next-generation borrow checker for the Rust programming language. Rust's distinguishing feature is its ability to guarantee memory safety through its type system and borrow checker, ensuring safety without impacting runtime performance. The current implementation, known as NLL (Non-Lexical Lifetimes), remains overly conservative in certain cases -- consequently, Rust developers have introduced a new version called Polonius, which is based on a more precise data-flow analysis. However, Polonius lacks an official specification, and information regarding its workings remains scattered. The goal of this thesis is to establish a mathematical framework that enables a clear understanding of this new implementation. This is approached using sets and logical statements, describing the rules established in various sources through predicates and inference rules. The final result is a simplified but formal description of Polonius. Rust Polonius preverjevalnik izposoj formalizacija Rust Polonius borrow checker formalization true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2026-06-09 14:25:05 2026-06-09 14:25:14 2026-07-23 08:21:01 0000-00-00 00:00:00 2026 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 38857 285772035 Trplan_Filip_-_Formalizacija_originalne_formulacije_Poloniusa.pdf Trplan_Filip_-_Formalizacija_originalne_formulacije_Poloniusa.pdf 1 26F38AEA80D95A29F969F3E52879A9BD 8106197c7931eb705212b73be185438391246189be73236b1166871aba98e0ed 448655d3-63fe-11f1-9b0d-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=235212 Fakulteta za računalništvo in informatiko 0 0 0