Software Composition - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Ouvrage (Y Compris Édition Critique Et Traduction) Année : 2013

Software Composition

Walter Binder
  • Fonction : Auteur
  • PersonId : 1004355
Welf Löwe
  • Fonction : Auteur
  • PersonId : 1004357

Résumé

We address the problem of verification of program terms parameterized by a data type X, such that the only operations involving X a program can perform are to input, output, and assign values of type X, as well as to test for equality such values. Such terms are said to be data independent with respect to X. Logical relations for game semantics of terms are defined, and it is shown that the Basic Lemma holds for them. This proves that terms are predicatively parametrically polymorphic, and it provides threshold collections, i.e. sufficiently large finite interpretations of X, for the problem of verification of observational-equivalence, approximation, and safety of parameterized terms for all interpretations of X. In this way we can verify terms with data independent infinite integer types. The practicality of the approach is evaluated on several examples.
BookFrontmatter.pdf (284.84 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01492781 , version 1 (20-03-2017)

Licence

Paternité

Identifiants

Citer

Walter Binder, Eric Bodden, Welf Löwe. Software Composition: 12th International Conference, SC 2013, Budapest, Hungary, June 19, 2013. Springer, LNCS-8088, 2013, Lecture Notes in Computer Science, 978-3-642-39613-7. ⟨10.1007/978-3-642-39614-4⟩. ⟨hal-01492781⟩
190 Consultations
67 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More