Preverjenje pravilnosti programov z odvisnimi tipi v programskem jeziku Idris

Repas, Blaž (author), Mihelič, Jurij (mentor)

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.

• Language: Slovenian
• Keywords: odvisni tipi, pravilnost programov, programski jezik Idris
• Work type: Bachelor thesis/paper
• Organization: FRI - Faculty of Computer and Information Science
• Year: 2014
• PID: 20.500.12556/RUL-29468
• Publication date in RUL: 16.09.2014

Secondary language

• Language: English
• Title: Verifying correctness of programs with dependent types in Idris programming language

Abstract

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.

• Keywords: dependent types, program correctness, Idris programming language