Verjetnostna separacijska logika

Jereb, Janez Ignacij (author), Simpson, Alexander Keith (mentor)

To delo obravnava programsko verjetnostno separacijsko logiko in jo razvije z novo semantiko programskega jezika, logičnih formul ter novim pravilom okvirja. Sintaksi programskega jezika so dodani tipi, medtem ko je za semantiko programskega jezika uporabljena monadna denotacijska semantika. Zanjo je potrebna uporaba teorije domen, ki je v tem delu tudi na kratko predstavljena. Semantika jezika je razširjena tudi z nedefiniranimi spremenljivkami. Logika pa je razširjena s tretjo resničnostno vrednostjo — nedefinirano. Pravilo okvirja se bistveno poenostavi z odstranitvijo večine stranskih pogojev. Dokazana je pravilnost poenostavljene različice pravila okvirja. Prav tako je prikazana uporaba logike na primerih kriptografskih protokolov.

• Language: Slovenian
• Keywords: separacijska logika, denotacijska semantika, trovrednostna logika, tipni sistem, verjetnostno programiranje, dokazovanje pravilnosti, verjetnostna neodvisnost
• Work type: Bachelor thesis/paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FRI - Faculty of Computer and Information Science
• Year: 2025
• PID: 20.500.12556/RUL-170333
• COBISS.SI-ID: 241427715
• Publication date in RUL: 03.07.2025

Secondary language

• Language: English
• Title: Probabilistic Separation Logic

Abstract

This work addresses Probabilistic Separation Logic and develops it with new semantics for the programming language and logic formulas together with a new frame rule. Types are added to the syntax. For the semantics of the programming language the monadic denotational semantics is used. It requires domain theory which is also briefly presented. The logic is expanded with a third truth value — undefined. The frame rule is significantly simplified with the removal of side conditions. The correctness of the simplified version of the frame rule is proved. The use of logic is presented on examples of cryptographic protocols.

• Keywords: separation logic, denotational semantics, three-value logic, type system, probabilistic programming, proving program correctness, probabilistic independence