Mandatory and Potential Choice: Comparing Event-B and STAIRS

Abstract. In order to decide whether a software system fulfills a specification, or whether a detailed specification preserves the properties of a more abstract specification, we need an understanding of what it means for one specification to fulfill another specification. This is particularly important when the specification contains one or more operators for expressing choice. Operators for choice have been studied for more than three decades …