Archivio Istituzionale della RicercaThe SPIN extension presented in this article is meant as a way to facilitate the modeling and verification of object-oriented programs. It provides means for the formal representation of some run-time mechanisms intensively used in OO software, such as dynamic object creation and deletion, virtual function calls, etc. This article presents a number of language extensions along with their implementation in SPIN. We carried out a number of experiments and found out that an important expressibility gain can be achieved with at most a small loss of performance.
dSPIN: A Dynamic Extension of SPIN / Demartini, Claudio Giovanni; R., Iosif; Sisto, Riccardo. - 1680:(1999), pp. 261-276. (Intervento presentato al convegno 5th and 6th International SPIN Workshops tenutosi a Trento (ITA). Toulouse (FRA) nel July 5, 1999. September 21 and 24, 1999) [10.1007/3-540-48234-2_20].
dSPIN: A Dynamic Extension of SPIN
DEMARTINI, Claudio Giovanni;SISTO, Riccardo
1999
Abstract
The SPIN extension presented in this article is meant as a way to facilitate the modeling and verification of object-oriented programs. It provides means for the formal representation of some run-time mechanisms intensively used in OO software, such as dynamic object creation and deletion, virtual function calls, etc. This article presents a number of language extensions along with their implementation in SPIN. We carried out a number of experiments and found out that an important expressibility gain can be achieved with at most a small loss of performance.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/1410894
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo