Extending the Sparkle Core language with object abstraction

Sparkle is a theorem prover specially constructed for the functional programming language Clean. In a pure functional language like Clean the variables represent constant values; variables do not change in time. Hence it seems that temporality has no meaning in functional programs. However, in certa...

Teljes leírás

Elmentve itt :
Bibliográfiai részletek
Szerzők: Tejfel Máté
Horváth Zoltán
Kozsik Tamás
Testületi szerző: Conference for PhD Students in Computer Science (4.) (2004) (Szeged)
Dokumentumtípus: Cikk
Megjelent: 2005
Sorozat:Acta cybernetica 17 No. 2
Kulcsszavak:Számítástechnika, Kibernetika
Tárgyszavak:
Online Access:http://acta.bibl.u-szeged.hu/12774
LEADER 01835nab a2200253 i 4500
001 acta12774
005 20220615125622.0
008 161015s2005 hu o 0|| eng d
022 |a 0324-721X 
040 |a SZTE Egyetemi Kiadványok Repozitórium  |b hun 
041 |a eng 
100 1 |a Tejfel Máté 
245 1 0 |a Extending the Sparkle Core language with object abstraction  |h [elektronikus dokumentum] /  |c  Tejfel Máté 
260 |c 2005 
300 |a 419-445 
490 0 |a Acta cybernetica  |v 17 No. 2 
520 3 |a Sparkle is a theorem prover specially constructed for the functional programming language Clean. In a pure functional language like Clean the variables represent constant values; variables do not change in time. Hence it seems that temporality has no meaning in functional programs. However, in certain cases (e.g. in interactive or distributed programs, or in ones that use I/O), a series of values computed from one another can be considered as different states of the same "abstract object". For this abstract object temporal properties can be proved. This paper presents a method to describe abstract objects and invariant properties in an extended version of the Sparkle Core language. The creation of such descriptions will be supported by a refactoring tool. The descriptions are completely machine processible, and provide a way to automatize the proof of temporal properties of Clean programs with the extended Sparkle system. 
650 4 |a Természettudományok 
650 4 |a Számítás- és információtudomány 
695 |a Számítástechnika, Kibernetika 
700 0 1 |a Horváth Zoltán  |e aut 
700 0 1 |a Kozsik Tamás  |e aut 
710 |a Conference for PhD Students in Computer Science (4.) (2004) (Szeged) 
856 4 0 |u http://acta.bibl.u-szeged.hu/12774/1/Tejfel_2005_ActaCybernetica.pdf  |z Dokumentum-elérés