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. Acta cybernetica, (17) 2. pp. 419-445. (2005)

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

Download (225kB)

Abstract

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
Event Title: Conference for PhD Students in Computer Science, 4., 2004, Szeged
Journal or Publication Title: Acta cybernetica
Date: 2005
Volume: 17
Number: 2
Page Range: pp. 419-445
ISSN: 0324-721X
Language: angol
Uncontrolled Keywords: Természettudomány, Informatika
Additional Information: Bibliogr.: p. 436-438.; Abstract
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2018. Jun. 05. 15:02
URI: http://acta.bibl.u-szeged.hu/id/eprint/12774

Actions (login required)

View Item View Item