20.500.12556/RUL-29468 Preverjenje pravilnosti programov z odvisnimi tipi v programskem jeziku Idris Verifying correctness of programs with dependent types in Idris programming language Formalno dokazovanje pravilnosti programov se v ključnih primerih izvaja ročno. Programski jeziki z odvisnimi tipi kot logična ogrodja predstavljajo avtomatizirano alternativo ročnemu preverjanju pravilnosti. V tem diplomskem delu obravnavamo sisteme tipov ter programske jezike z odvisnimi tipi. Predstavimo programski jezik Idris, ki podpira poljubno kompleksne odvisne tipe. Pokažemo, kako izjave pretvoriti v tipe funkcij in jih z implementacijo funkcij dokazati, pravilnost pa avtomatsko preverja prevajalnik. S pomočjo odvisnih tipov podamo avtomatsko preverjene implementacije podatkovnih struktur seznam, sklad in vrsta. Poglobimo se v algoritem urejanja z vstavljanjem. Z dokazom linearne urejenosti naravnih števil dokažemo, da je njegov izhod urejen seznam, z dokazom permutiranosti pa pokažemo, da je izhodni seznam permutacija vhodnega. Formal verification of program correctness in mission critical applications is still done manually. Programming languages with dependent types used as logical frameworks present an alternative to manual verification of correctness. In this thesis we deal with type systems and programming languages with dependent types. We introduce the Idris programming language which supports arbitrarily complex dependent types. We show how to translate propositions into function types and how to prove them by implementing the functions. Correctness is then automatically verified by the compiler. With use of dependent types we provide automatically verified implementations of data structures like list, stack and queue. To demonstrate usefulness of dependent types we provide automatically verified implementation of insertion sort algorithm. We prove sortedness with linear order of natural numbers and also that the output list is a permutation of the input list. odvisni tipi pravilnost programov programski jezik Idris dependent types program correctness Idris programming language true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2014-09-16 15:45:01 2014-09-16 15:45:01 2022-08-01 10:42:18 0000-00-00 00:00:00 2014 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 14461 63110341-20140908153452-diploma_Repar.pdf 63110341-20140908153452-diploma_Repar.pdf 1 3755D6CF290C4A0B7B2A48786EBF280B eb39a5d09cf25abc15021412afa859a5d5418f56d980636412c09ecbf67b386d 4a4cd3d9-a1a8-11eb-a523-00155dcfd717 20.500.12556/rul/4ad7598e-6bd2-483a-a97e-042b2e3c1bee https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=29464 Fakulteta za računalništvo in informatiko 0 0 0