257 KB20 KB200820262017Koprivec, Filipštevilka:3letnik:64str. 81-90ISSN:0473-7466COBISSID:18138201URN:URN:NBN:SI:doc-PPKGZTCMslDruštvo matematikov, fizikov in astronomov SlovenijeObzornik za matematiko in fizikoizreki o varnostiizvajanjeprogramski jeziksintaksatipiTipi v programskih jezikih in izreki o varnosti programov|One of the most important tools in programming is definitely the type system, which allows us to eliminate a whole class of errors before the actual evaluation od the program even takes place. The article presents a simple programming language which is used to examine syntax and evaluation rules, and proceeds with proving a safety theorem which uses types to ensure that the program state will stay sound during the execution. Simply type lambda calculus and the corresponding safety theorem are presented at the endEno izmed pomembnejših orodij v programiranju so zagotovi tipi, saj nam omogočajo, da že pred zagonom programa preprečimo določeno vrsto napak. V članku si na primeru preprostega programskega jezika najprej ogledamo pravila sintakse in izvajanja, nato pa zanj dokažemo izrek o varnosti, ki nam s pomočjo tipov zagotavlja, da bo med izvajanjem programa njegovo stanje vedno smiselno. Na kratko predstavimo tudi lambda račun z enostavnimi tipi in njemu pripadajoči izrek o varnostiTEXTznanstveno časopisjejournalsSlovenian National E-content AggregatorNational and University Library of SloveniaDruštvo matematikov, fizikov in astronomov