Your browser does not allow JavaScript!
JavaScript is necessary for the proper functioning of this website. Please enable JavaScript or use a modern browser.
Open Science Slovenia
Open Science
DiKUL
slv
|
eng
Search
Browse
New in RUL
About RUL
In numbers
Help
Sign in
Preverjanje pravilnosti programov z odvisnimi tipi v programskem jeziku Idris : diplomsko delo
ID
Repas, Blaž
(
Author
),
ID
Mihelič, Jurij
(
Mentor
)
More about this mentor...
URL - Presentation file, Visit
http://eprints.fri.uni-lj.si/2665/
Image galllery
Abstract
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
,
računalništvo
,
računalništvo in informatika
,
univerzitetni študij
,
diplomske naloge
Work type:
Bachelor thesis/paper
Typology:
2.11 - Undergraduate Thesis
Organization:
FRI - Faculty of Computer and Information Science
Publisher:
[B. Repas]
Year:
2014
Number of pages:
77 str.
PID:
20.500.12556/RUL-68833
UDC:
004.42(043.2)
COBISS.SI-ID:
1536094403
Publication date in RUL:
10.07.2015
Views:
1625
Downloads:
239
Metadata:
Cite this work
Plain text
BibTeX
EndNote XML
EndNote/Refer
RIS
ABNT
ACM Ref
AMA
APA
Chicago 17th Author-Date
Harvard
IEEE
ISO 690
MLA
Vancouver
:
Copy citation
Share:
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
,
computer science
,
computer and information science
,
diploma
Similar documents
Similar works from RUL:
Similar works from other Slovenian collections:
Back