prikaz prve stranice dokumenta Hoareova logika
  Download
PDF 479.39 KB
master's thesis
Hoareova logika
2020. urn:nbn:hr:166:264314
Livaja, Petra
University of Split
Faculty of Science
Department of Mathematics

Cite this document

Livaja, P. (2020). Hoareova logika (Master's thesis). Split: University of Split, Faculty of Science. Retrieved from https://urn.nsk.hr/urn:nbn:hr:166:264314

Livaja, Petra. "Hoareova logika." Master's thesis, University of Split, Faculty of Science, 2020. https://urn.nsk.hr/urn:nbn:hr:166:264314

Livaja, Petra. "Hoareova logika." Master's thesis, University of Split, Faculty of Science, 2020. https://urn.nsk.hr/urn:nbn:hr:166:264314

Livaja, P. (2020). 'Hoareova logika', Master's thesis, University of Split, Faculty of Science, accessed 19 April 2024, https://urn.nsk.hr/urn:nbn:hr:166:264314

Livaja P. Hoareova logika [Master's thesis]. Split: University of Split, Faculty of Science; 2020 [cited 2024 April 19] Available at: https://urn.nsk.hr/urn:nbn:hr:166:264314

P. Livaja, "Hoareova logika", Master's thesis, University of Split, Faculty of Science, Split, 2020. Available at: https://urn.nsk.hr/urn:nbn:hr:166:264314

Please login to the repository to save this object to your list.
Metadata
TitleHoareova logika
Title (english)Hoare's logic
AuthorPetra Livaja
MentorJurica Perić (mentor)
Committee memberJurica Perić (predsjednik povjerenstva)
Committee memberMilica Klaričić Bakula (član povjerenstva)
Committee memberGoran Erceg (član povjerenstva)
GranterUniversity of Split
Faculty of Science
(Department of Mathematics)
Split
Defense date and country2020-12-18, Croatia
Scientific / art field,
discipline and subdiscipline		NATURAL SCIENCES
Mathematics
Mathematical Logic and Accounting
Abstract
U ovom diplomskom radu prezentiramo Hoareovu logiku koja daje pravila za odnos između tvrdnji o vrijednostima varijabli prije i nakon izvršavanja programa napisanog u IMP-u, tj. za provjeru parcijalne korektnosti. Proučavamo probleme utemeljenosti Hoareovih pravila i potpunosti. Obzirom da ona nasljeđuju nepotpunost iskazanu Gödelovim teoremom, u nastavku promatramo potpunost u Cook-ovom smislu i pritom odvajamo nepotpunost jezika Assn od nepotpunosti uzrokovane aksiomima i pravilima izgradnje programa. Postupno gradimo složenije sustave dodavajući nova pravila te im provjeravamo potpunost u Cook-ovom smislu i utemeljenost. Osim za while programe, dodajemo pravila za procedure bez parametara (za rekurzivne i nerekurzivne procedure), deklaraciju varijabli i osvrćemo se na problem s neinicijaliziranim varijablama, subskriptne varijable i mehanizme parametara, kod kojih promatramo poziv po imenu procedure
Abstract (english)
In this thesis, we present Hoare’s logic that provides rules for the relationship between assertions about the values of variables before and after the execution of a program written in IMP, i.e., to check partial correctness. We study the problems of the validity of Hoare’s rules and completeness. Since they inherit the incompleteness expressed by Gödel’s theorem, we observe the completeness in Cook’s sense below and separate the incompleteness of the Assn language from the incompleteness caused by axioms and rules of program construction. In addition to while programs, we add rules for non-parameter procedures (for recursive and non-recursive procedures), declaration of variables, and consider the problem with uninitialized variables, subscript variables, and parameter mechanisms, in which we observe the call by the name of the procedure.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:166:264314
Study programmeTitle: Mathematics; specializations in: major in pure mathematics, major in computing, major in teaching, major in statistics and computing
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 conditionsOpen access
Terms of useLicence In copyright icon
Created on2021-02-02 17:30:34