Programming language elements for correctness proofs

Dévai Gergely: Programming language elements for correctness proofs. In: Acta cybernetica, (18) 3. pp. 403-425. (2008)

Előnézet

Cikk, tanulmány, mű Devai_2008_ActaCybernetica.pdf Letöltés (246kB) | Előnézet

Absztrakt (kivonat)

Formal methods are not used widely in industrial software development, because the overhead of formally proving program properties is generally not acceptable. In this paper we present an ongoing research project to make the construction of such proofs easier by embedding the proof system into a compiler. Using the introduced new programming language, the programmer writes formal specification first. The specification is to be refined using stepwise refinement which results in a proof. The compiler checks this proof and generates the corresponding program in a traditional programming language. The resulting code automatically fulfills the requirements of the specification. In this paper we present language elements to build specification statements and proofs. We give a short overview on the metaprogramming techniques of the language that support the programmer's work. Using a formal model we give the semantics of specification statements and refinements. We also prove the soundness of the basic algorithms of the compiler.

Mű típusa:	Cikk, tanulmány, mű
Befoglaló folyóirat/kiadvány címe:	Acta cybernetica
Dátum:	2008
Kötet:	18
Szám:	3
ISSN:	0324-721X
Oldalak:	pp. 403-425
Nyelv:	angol
Kiadás helye:	Szeged
Konferencia neve:	Conference for PhD Students in Computer Science (5.) (2006) (Szeged)
Befoglaló mű URL:	http://acta.bibl.u-szeged.hu/38525/
Kulcsszavak:	Számítástechnika, Kibernetika
Megjegyzések:	Bibliogr.: p. 423-425. ; összefoglalás angol nyelven
Szakterület:	01. Természettudományok 01. Természettudományok > 01.02. Számítás- és információtudomány
Feltöltés dátuma:	2016. okt. 15. 12:25
Utolsó módosítás:	2022. jún. 16. 14:45
URI:	http://acta.bibl.u-szeged.hu/id/eprint/12827

Bővebben:

Tétel nézet