Lecture Notes in Computer Science, 1999, Volume 1708/1999, 709, DOI: 10.1007/3-540-48119-2_24

Interpreting the B-Method in the Refinement Calculus

Yann Rouzaud

View Related Documents

Abstract

In this paper,we study the B-Method in the light of the theory of refinement calculus. It allows us to explain the proof obligations for a refinement component in terms of standard data refinement. A second result is an improvement of the architectural condition of [PR98], ensuring global correctness of a B software system using the sees primitive.

Fulltext Preview

Image of the first page of the fulltext document