Correct‐by‐construction specification to verified code

Abstract Event‐B is a formal notation and method for the systems development. The key feature of this method is to produce correct‐by‐construction system designs. Once the correct design is establi...