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)
Preview |
Cikk, tanulmány, mű
Tejfel_2005_ActaCybernetica.pdf Download (225kB) | Preview |
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 |
|---|---|
| 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 |
