prikaz prve stranice dokumenta Aksiomatska semantika IMP-a
Pristup korisnicima matične ustanove
diplomski rad
Aksiomatska semantika IMP-a
2017. urn:nbn:hr:166:721201
Žmire, Damira
Sveučilište u Splitu
Prirodoslovno-matematički fakultet
Odjel za matematiku

Citirajte ovaj rad

Žmire, D. (2017). Aksiomatska semantika IMP-a (Diplomski rad). Split: Sveučilište u Splitu, Prirodoslovno-matematički fakultet. Preuzeto s https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, Damira. "Aksiomatska semantika IMP-a." Diplomski rad, Sveučilište u Splitu, Prirodoslovno-matematički fakultet, 2017. https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, Damira. "Aksiomatska semantika IMP-a." Diplomski rad, Sveučilište u Splitu, Prirodoslovno-matematički fakultet, 2017. https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, D. (2017). 'Aksiomatska semantika IMP-a', Diplomski rad, Sveučilište u Splitu, Prirodoslovno-matematički fakultet, citirano: 21.11.2024., https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire D. Aksiomatska semantika IMP-a [Diplomski rad]. Split: Sveučilište u Splitu, Prirodoslovno-matematički fakultet; 2017 [pristupljeno 21.11.2024.] Dostupno na: https://urn.nsk.hr/urn:nbn:hr:166:721201

D. Žmire, "Aksiomatska semantika IMP-a", Diplomski rad, Sveučilište u Splitu, Prirodoslovno-matematički fakultet, Split, 2017. Dostupno na: https://urn.nsk.hr/urn:nbn:hr:166:721201

Za citiranje koristite ovu mrežnu adresu: https://urn.nsk.hr/urn:nbn:hr:166:721201
Prijavite se u repozitorij kako biste mogli spremiti objekt u svoju listu.
Podaci o radu
NaslovAksiomatska semantika IMP-a
Naslov (engleski)The axiomatic semantics of IMP
AutorDamira Žmire
MentorMilica Klaričić Bakula (mentor)
Član povjerenstvaMilica Klaričić Bakula (predsjednik povjerenstva)
Član povjerenstvaJurica Perić (član povjerenstva)
Član povjerenstvaMarija Bliznac Trebješanin (član povjerenstva)
Ustanova koja je dodijelila
akademski / stručni stupanj		Sveučilište u Splitu
Prirodoslovno-matematički fakultet
(Odjel za matematiku)
Split
Datum i država obrane2017-09-27, Hrvatska
Znanstveno / umjetničko
područje, polje i grana		PRIRODNE ZNANOSTI
Matematika
Sažetak
U ovom diplomskom radu proučavamo aksiomatsku semantiku IMP-a. Ba vimo se sustavnom provjerom programa napisanih u IMP-u. Uvedena su Hoareova pravila za provjeru parcijalne korektnosti programa te je dokazana utemeljenost Hoareove logike. Navedeno je uključivalo proširenje booleovih izraza do bogatijeg jezika tvrdnji o programskim stanjima. Nadalje, razmatrali smo pitanje potpunosti Hoareovih pravila. Godelov teorem nepotpunosti ukazuje na to da ne postoji potpun sustav dokazivanja kojim bi se utvrdile sve valjane tvrdnje. Hoareova pravila nasljeduju ovu nepotpunost. Medutim, ako odvojimo nepotpunost jezika tvrdnji od nepotpunosti uzrokovane aksiomima i pravilima za konstrukciju programa, možemo doći do Cookove relativne potpunosti. Dokaz relativne potpunosti Hoareove logike oslanja se na ideju o najslabijem (slobodnom) preduvjetu i vodi do razmatranja uvjeta istinitosti.
Sažetak (engleski)
In this master’s thesis we study the axiomatic semantics of IMP. We turn to the business of systematic verification of programs in IMP. The Hoare ru les for showing the partial correctness of programs are introduced and shown sound. This involves extending the boolean expressions to a rich language of assertions about program states. Further, it is discussed what it means for the Hoare rules to be complete. Godel’s Incompleteness Theorem implies there is no complete proof system for establishing precisely the valid assertions. The Hoare rules inherit this incompleteness. However, by separating incomple teness of the assertion language from incompleteness due to inadequacies in the axioms and rules for the programming language constructs, we can obtain relative completeness in the sense of Cook. The proof that the Hoare rules are relatively complete relies on the idea of weakest (liberal) precondition and leads into a discussion of verification-condition generators.
Ključne riječi
Ključne riječi (engleski)
Jezikhrvatski
URN:NBNurn:nbn:hr:166:721201
Studijski programNaziv: Matematika; smjerovi: teorijski, računarski, nastavnički
Smjer: računarski
Vrsta studija: sveučilišni
Stupanj studija: diplomski
Akademski / stručni naziv: magistar/magistra matematike (mag. math.)
Vrsta resursaTekst
Način izrade datotekeIzvorno digitalna
Prava pristupaPristup korisnicima matične ustanove
Uvjeti korištenjaIkona licence Zaštićeno autorskim pravom.
Datum i vrijeme pohrane2018-05-18 16:01:49