Extending the Sparkle Core language with object abstraction

Tejfel Máté and Horváth Zoltán and Kozsik Tamás: Extending the Sparkle Core language with object abstraction. In: Acta cybernetica, (17) 2. pp. 419-445. (2005)

[thumbnail of Tejfel_2005_ActaCybernetica.pdf]
Cikk, tanulmány, mű

Download (225kB) | Preview


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.

Item Type: Article
Journal or Publication Title: Acta cybernetica
Date: 2005
Volume: 17
Number: 2
ISSN: 0324-721X
Page Range: pp. 419-445
Language: English
Place of Publication: Szeged
Event Title: Conference for PhD Students in Computer Science (4.) (2004) (Szeged)
Related URLs: http://acta.bibl.u-szeged.hu/38520/
Uncontrolled Keywords: Számítástechnika, Kibernetika
Additional Information: Bibliogr.: p. 436-438. ; összefoglalás angol nyelven
Subjects: 01. Natural sciences
01. Natural sciences > 01.02. Computer and information sciences
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2022. Jun. 15. 12:56
URI: http://acta.bibl.u-szeged.hu/id/eprint/12774

Actions (login required)

View Item View Item