Proving the Correctness of Algebraically Specified Software: Modularity and Observability Issues
Gilles Bernot, Michel Bidoit · 1991
We investigate how far modularity and observability issues can contribute to a better understanding of software correctness. We detail the impact of modularity on the semantics of algebraic specifications and we show that, with the stratified loose semantics, software correctness can be established on a module per module basis. We discuss observability issues and we introduce an observational semantics where sort observation is refined by specifying that some operations do not allow observations. Then the stratified loose approach and our observational semantics are integrated together. As a result, we obtain a framework (mod-ular observational specifications) where the definition of software correctness is adequate, i.e. fits with actual software correctness. 1