Logotipo del repositorio
 

Reasoning tradeoffs in languages with enhanced modularity features

Fecha

2016-03

Autores

Sánchez Salazar, José
Leavens, Gary

Título de la revista

ISSN de la revista

Título del volumen

Editor

Modularity 2016: Proceedings of the 15th International Conference on Modularity 13-24 2016

Resumen

The continuous need for more ambitious, more complex, and more dependable software systems demands mechanisms to modularize such systems and reason about their correctness. The reasoning process is affected by the programming language's features, like dynamic dispatching, implicit invocation and oblivious aspect weaving, and by how the programmer uses them. In this paper, by devising a unifying formal setting, we show how reasoning varies with the different language mechanisms, and provide sound rules for reasoning about programs that use these features. While analyzing these mechanisms we explore the main compromises or tradeoffs that led to them and explain the disciplines they impose and the strength of the reasoning conclusions one can derive in each case. Our contributions will benefit both language designers and programmers. Language designers will benefit from learning the effects of different modularity features on reasoning. Programmers will learn how to reason about programs that use such features. © 2016 ACM.
The continuous need for more ambitious, more complex, and more dependable software systems demands mechanisms to modularize such systems and reason about their correctness. The reasoning process is affected by the programming language’s features, like dynamic dispatching, implicit invocation and oblivious aspect weaving, and by how the programmer uses them. In this paper, by devising a unifying formal setting, we show how reasoning varies with the different language mechanisms, and provide sound rules for reasoning about programs that use these features. While analyzing these mechanisms we explore the main compromises or tradeoffs that led to them and explain the disciplines they impose and the strength of the reasoning conclusions one can derive in each case. Our contributions will benefit both language designers and programmers. Language designers will benefit from learning the effects of different modularity features on reasoning. Programmers will learn how to reason about programs that use such features.

Descripción

Palabras clave

SOFTWARE, COMPUTACIÓN, MODULE VERIFICATION, CROSS-COMPUTATION TOOLS AND TECHINIQUES, ENGINEERING, SOFTWARE CREATION AND MANAGEMENT

Citación