prikaz prve stranice dokumenta Aksiomatska semantika IMP-a
Access restricted to students and staff of home institution
master's thesis
Aksiomatska semantika IMP-a
2017. urn:nbn:hr:166:721201
Žmire, Damira
University of Split
Faculty of Science
Department of Mathematics

Cite this document

Žmire, D. (2017). Aksiomatska semantika IMP-a (Master's thesis). Split: University of Split, Faculty of Science. Retrieved from https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, Damira. "Aksiomatska semantika IMP-a." Master's thesis, University of Split, Faculty of Science, 2017. https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, Damira. "Aksiomatska semantika IMP-a." Master's thesis, University of Split, Faculty of Science, 2017. https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire, D. (2017). 'Aksiomatska semantika IMP-a', Master's thesis, University of Split, Faculty of Science, accessed 19 April 2024, https://urn.nsk.hr/urn:nbn:hr:166:721201

Žmire D. Aksiomatska semantika IMP-a [Master's thesis]. Split: University of Split, Faculty of Science; 2017 [cited 2024 April 19] Available at: https://urn.nsk.hr/urn:nbn:hr:166:721201

D. Žmire, "Aksiomatska semantika IMP-a", Master's thesis, University of Split, Faculty of Science, Split, 2017. Available at: https://urn.nsk.hr/urn:nbn:hr:166:721201

Please login to the repository to save this object to your list.
Metadata
TitleAksiomatska semantika IMP-a
Title (english)The axiomatic semantics of IMP
AuthorDamira Žmire
MentorMilica Klaričić Bakula (mentor)
Committee memberMilica Klaričić Bakula (predsjednik povjerenstva)
Committee memberJurica Perić (član povjerenstva)
Committee memberMarija Bliznac Trebješanin (član povjerenstva)
GranterUniversity of Split
Faculty of Science
(Department of Mathematics)
Split
Defense date and country2017-09-27, Croatia
Scientific / art field,
discipline and subdiscipline		NATURAL SCIENCES
Mathematics
Abstract
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.
Abstract (english)
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.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:166:721201
Study programmeTitle: Mathematics; specializations in: major in pure mathematics, major in computing, major in teaching
Course: major in computing
Study programme type: university
Study level: graduate
Academic / professional title: magistar/magistra matematike (magistar/magistra matematike)
Type of resourceText
File originBorn digital
Access conditionsAccess restricted to students and staff of home institution
Terms of useLicence In copyright icon
Created on2018-05-18 16:01:49