Vaš brskalnik ne omogoča JavaScript!
JavaScript je nujen za pravilno delovanje teh spletnih strani. Omogočite JavaScript ali pa uporabite sodobnejši brskalnik.
Nacionalni portal odprte znanosti
Odprta znanost
DiKUL
slv
|
eng
Iskanje
Brskanje
Novo v RUL
Kaj je RUL
V številkah
Pomoč
Prijava
Preverjanje pravilnosti programov z odvisnimi tipi v programskem jeziku Idris : diplomsko delo
ID
Repas, Blaž
(
Avtor
),
ID
Mihelič, Jurij
(
Mentor
)
Več o mentorju...
URL - Predstavitvena datoteka, za dostop obiščite
http://eprints.fri.uni-lj.si/2665/
Galerija slik
Izvleček
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.
Jezik:
Slovenski jezik
Ključne besede:
odvisni tipi
,
pravilnost programov
,
programski jezik Idris
,
računalništvo
,
računalništvo in informatika
,
univerzitetni študij
,
diplomske naloge
Vrsta gradiva:
Diplomsko delo/naloga
Tipologija:
2.11 - Diplomsko delo
Organizacija:
FRI - Fakulteta za računalništvo in informatiko
Založnik:
[B. Repas]
Leto izida:
2014
Št. strani:
77 str.
PID:
20.500.12556/RUL-68833
UDK:
004.42(043.2)
COBISS.SI-ID:
1536094403
Datum objave v RUL:
10.07.2015
Število ogledov:
1638
Število prenosov:
239
Metapodatki:
Citiraj gradivo
Navadno besedilo
BibTeX
EndNote XML
EndNote/Refer
RIS
ABNT
ACM Ref
AMA
APA
Chicago 17th Author-Date
Harvard
IEEE
ISO 690
MLA
Vancouver
:
Kopiraj citat
Objavi na:
Sekundarni jezik
Jezik:
Angleški jezik
Naslov:
Verifying correctness of programs with dependent types in Idris programming language
Izvleček:
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.
Ključne besede:
dependent types
,
program correctness
,
Idris programming language
,
computer science
,
computer and information science
,
diploma
Podobna dela
Podobna dela v RUL:
Podobna dela v drugih slovenskih zbirkah:
Nazaj