Show simple item record

Consultant
dc.contributor.advisor
Csörnyei, Zoltán
Author
dc.contributor.author
Dévai, Gergely 
Availability Date
dc.date.accessioned
2019-02-08T08:22:50Z
Availability Date
dc.date.available
2019-02-08T08:22:50Z
Release
dc.date.issued
2017
uri
dc.identifier.uri
http://hdl.handle.net/10831/37858
Abstract
dc.description.abstract
A dolgozat első tézise egy formális programmodellt vezet be haladási és biztonsági kritériumok megfogalmazására alkalmas temporális logikai operátorokkal. A modell levezetési szabályai bizonyítással együtt kerülnek bemutatásra. A bizonyított tételeken alapszik az az algoritmus, amely képes ellenőrizni a modellben felírt levezetések helyességét. A formális modell használatát egy Haskellbe ágyazott nyelv teszi lehetővé. Ennek kapcsán a dolgozat elemzi a Haskellben lehetséges nyelvbeágyazási technikákat. A megalkotott nyelv használatát a C++ egyes utasításainak specifikációja és egyszerű C++ programok levezetése demonstrálja. A második tézis a funkcionális nyelvek mintaillesztésének egy hiányosságával foglalkozik. Részletesen elemezi a beágyazott programokra történő mintaillesztés lehetőségeit funkcionális nyelvekben, és megmutatja, hogy ezek egyike sem nyújt kielégítő megoldást. A megoldás első lépése a korlátozott függvényminták fogalmának kidolgozása, amely a Curry nyelvből ismert függvényminták megszorítása. A korlátozott függvényminták szemantikája és implementációja a funkcionális nyelvek klasszikus mintaillesztésére visszavezethető. A korlátozott függvényminták alkalmasak a listaprefix minták, az n+k minták és a polimorf számliterálokra történő mintaillesztés egységes, konzisztens megvalósítására. A dolgozat bizonyítja, hogy a korlátozott függvényminta tulajdonság nem eldönthető. Ezért a megoldás második eleme az ellenőrizhető függvényminták bevezetése. Ez a fogalom egy döntési eljáráson alapszik, amely a korlátozott függvényminták egy szigorú részhalmazát fogadja el, és garantáltan terminál. Az elfogadott részhalmazban valamennyi korábban felsorolt használati eset benne van, és a döntési eljárás fordítóprogramokba beépíthető. A nyelvi kiterjesztés használata fordítóprogramba épített támogatás nélkül is haszálható egy függvénykönyvtár segítségével. A harmadik tézis a korábban bevezetett technikákat a formális szoftverfejlesztés egyes nemtriviális problémáinak megoldására használja. A dolgozat megmutatja, hogy a bizonyítások előállítására használt metaprogramozás biztonságos és hatékony eszköz. Bizonyítássablonokat ad egyes klasszikus matematikai bizonyítási technikákhoz és programkonstrukciók levezetési szabályaihoz. A kidolgozott rendszerben lehetőség nyílik dinamikus memóriát és mutatókat használó programok levezetésére az elválasztó logika hatékony bizonyítási stílusát használva. Axiomatizálhatók továbbá a C++ Standard Template Library konténereinek és bejáróinak műveletei.hu_HU
Language
dc.language
magyarhu_HU
Title
dc.title
Programhelyesség- bizonyítás fordítási időbenhu_HU
Type
dc.type
doktori dolgozat
Language
dc.language.rfc3066
hun
Rights
dc.rights.holder
A doktori disszertációk szerzői jogvédelem alatt állnak, csak a szerzői jogok maradéktalan tiszteletben tartásával használhatók.hu_HU
Abstract in English
dc.description.abstracteng
The first thesis introduces a formal programming model with temporal logic operators to express progress and safety criteria. The presented refinement rules are proved to be sound. These rules form the basis of the algorithm that can be used to check the correctness of derivation sequences expressed in the model. A embedded language in Haskell is introduced to facilitate the practical use of the formal model. In connection with this, the thesis analyse the language embedding techniques possible in Haskell. Specification of selected C++ instructions and the derivation of simple, correct-by-construction C++ program fragments demonstrate the use of the system. The second thesis is motivated by a shortcoming of the pattern matching of functional languages. Different possibilities of pattern matching on embedded programs in functional languages are analysed in depth, and it is shown that, none of these provide satisfactory solutions. The first step of the solution is to introduce the notion of restricted function patterns, being a limited version of function patterns known from the Curry language. The semantics and implementation of restricted function patterns can be based on the classical pattern matching in functional languages. The restricted function patterns are suitable to provide list prefix patterns, n+k patterns and polymorphic numeric literals in a consistent way. The thesis proves that the restricted function pattern property is undecidable. For this reason, the second step of the solution is the introduction of decidable function patterns. This notion is based on a decision algorithm, which is guaranteed to terminate, and accepts a proper subset of the restricted function patterns. All earlier listed use cases fall into the accepted category, and the decision algorithm could be built into compilers. It is even possible to use the language extension without proper compiler support via a library. The third thesis uses these elaborated techniques to solve non-trivial problems of formal software development. The thesis argues that metaprogramming is a safe and performant technique, if used for the generation of proofs. Proof templates are defined for classical proof techniques and program derivation. The system is expressive enough to be used to derive programs using dynamic memory management and pointers in the powerful style of separation logic. Axioms of selected container and iterator instructions of the C++ Standard Template Library are also given.hu_HU
Name of Committee Member (a title, degree)
dc.description.commemb
Király Roland, főiskolai docens, PhDhu_HU
Name of Committee Member (a title, degree)
dc.description.commemb
Dömösi Pál (professor emeritus, PhD)hu_HU
Name of Committee Member (a title, degree)
dc.description.commemb
Fülöp Zoltán (egyetemi tanár, PhD)hu_HU
Name of Committee Member (a title, degree)
dc.description.commemb
Majzik István (egyetemi docens, PhD, dr. habil.)hu_HU
Official reviewer (a title, degree)
dc.description.reviewer
Aszalós László (egyetemi docens, phd)hu_HU
Official reviewer (a title, degree)
dc.description.reviewer
Fóthi Ákos (egyetemi docens, phd)hu_HU
Scope
dc.format.page
150hu_HU
Doi ID
dc.identifier.doi
10.15476/ELTE.2017.042
MTMT ID
dc.identifier.mtmt
3192605
Opac ID
dc.identifier.opac
http://opac.elte.hu/F?func=direct&doc_number=942284
Language
dc.language.other
angolhu_HU
Language
dc.language.other
magyarhu_HU
Discipline Discipline +
dc.subject.discipline
Műszaki tudományok/Informatikai tudományokhu_HU
Keyword English
dc.subject.en
program correctness proofhu_HU
Keyword English
dc.subject.en
specificationhu_HU
Keyword English
dc.subject.en
Haskellhu_HU
Keyword English
dc.subject.en
language embeddinghu_HU
Keyword English
dc.subject.en
function patternhu_HU
Keyword English
dc.subject.en
separation logichu_HU
Graduate schools / programs
dc.subject.prog
Informatika D. I./Az informatika alapjai és módszerei.hu_HU
Title in other languages ​​
dc.title.translated
Proving Program Correctness in Compilation Timehu_HU
Class
dc.type.genre
phdhu_HU
Type
dc.type.resrep
Tudományoshu_HU
Author
dc.contributor.inst
ELTE IK PHD/Informatika D. I.hu_HU
Goalkeeping Day
dc.date.defended
2017-06-27
Keywords
dc.subject.hu
programhelyességbizonyításhu_HU
Keywords
dc.subject.hu
specifikációhu_HU
Keywords
dc.subject.hu
Haskellhu_HU
Keywords
dc.subject.hu
nyelvbeágyazáshu_HU
Keywords
dc.subject.hu
függvénymintahu_HU
Keywords
dc.subject.hu
elválasztó logikahu_HU
Chairman of the Evaluation Committee (a title, degree)
dc.description.compres
Benczúr András (professor emeritus, DSc)hu_HU
Resolution dated
dc.date.decreedate
2018-03-08
date of submission
dc.date.presented
2017-03-20


Files in this item

Programhelyesség- bizonyítás fordítási időben
Programhelyesség- bizonyítás fordítási időben
Programhelyesség- bizonyítás fordítási időben
 

This item appears in the following Collection(s)

Show simple item record